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

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

tests
0

failures
0

ignored
10m51.88s

duration
100%

successful

Tests

Test Method name Duration Result
powPositive data()[100] 3.064s passed
powPositiveConcrete data()[101] 3.068s passed
powGeq1Concrete data()[102] 3.054s passed
pow2InIntLower data()[103] 3.046s passed
pow2InIntUpper data()[104] 3.066s passed
logSelfConcrete data()[105] 3.059s passed
log1Concrete data()[106] 3.071s passed
logProduct data()[107] 3.082s passed
logTimesBaseConcrete data()[108] 3.051s passed
logProdIdentity data()[109] 3.083s passed
moduloByteIsInByte data()[10] 3.140s passed
logProdIdentityConcrete data()[110] 3.050s passed
logPowIdentity data()[111] 3.069s passed
logPowIdentityConcrete data()[112] 3.053s passed
logPositive data()[113] 3.079s passed
logPositiveConcrete data()[114] 3.052s passed
logMono data()[115] 3.098s passed
logMonoConcrete data()[116] 3.061s passed
powLogLess data()[117] 3.104s passed
powLogMore2 data()[118] 3.084s passed
logLessThanPow data()[119] 3.105s passed
moduloCharIsInChar data()[11] 3.147s passed
logLessThanPowConcrete data()[120] 3.062s passed
logSqueeze data()[121] 3.079s passed
ifthenelse_equals data()[122] 3.057s passed
ifthenelse_equals_1 data()[123] 3.081s passed
ifthenelse_equals_2 data()[124] 3.052s passed
disjointWithSingleton1 data()[125] 3.072s passed
disjointWithSingleton2 data()[126] 3.074s passed
disjointArrayRanges data()[127] 3.085s passed
disjointArrayRangeAllFields1 data()[128] 3.091s passed
disjointArrayRangeAllFields2 data()[129] 3.086s passed
div_unique1 data()[12] 3.198s passed
seqSelfDefinition data()[130] 3.078s passed
seqOutsideValue data()[131] 3.092s passed
castedGetAny data()[132] 3.099s passed
seqGetAlphaCast data()[133] 3.073s passed
getOfSeqSingleton data()[134] 3.089s passed
getOfSeqSingletonConcrete data()[135] 3.098s passed
getOfSeqConcat data()[136] 3.072s passed
getOfSeqSub data()[137] 3.096s passed
getOfSeqReverse data()[138] 3.097s passed
lenOfSeqEmpty data()[139] 3.095s passed
div_unique2 data()[13] 3.172s passed
lenOfSeqSingleton data()[140] 3.090s passed
lenOfSeqConcat data()[141] 3.106s passed
lenOfSeqSub data()[142] 3.097s passed
lenOfSeqReverse data()[143] 3.105s passed
equalityToSeqGetAndSeqLenLeft data()[144] 3.104s passed
equalityToSeqGetAndSeqLenRight data()[145] 3.082s passed
getOfSeqSingletonEQ data()[146] 3.102s passed
getOfSeqConcatEQ data()[147] 3.102s passed
getOfSeqSubEQ data()[148] 3.419s passed
getOfSeqReverseEQ data()[149] 3.464s passed
div_exists data()[14] 3.312s passed
lenOfSeqEmptyEQ data()[150] 3.687s passed
lenOfSeqSingletonEQ data()[151] 3.454s passed
lenOfSeqConcatEQ data()[152] 3.643s passed
lenOfSeqSubEQ data()[153] 3.597s passed
lenOfSeqReverseEQ data()[154] 3.565s passed
getOfSeqDefEQ data()[155] 3.596s passed
lenOfSeqDefEQ data()[156] 3.536s passed
seqConcatWithSeqEmpty1 data()[157] 3.645s passed
seqConcatWithSeqEmpty2 data()[158] 3.763s passed
seqReverseOfSeqEmpty data()[159] 3.604s passed
div_one data()[15] 3.104s passed
subSeqComplete data()[160] 3.687s passed
subSeqTailR data()[161] 3.667s passed
subSeqTailL data()[162] 3.493s passed
subSeqTailEQR data()[163] 3.648s passed
subSeqTailEQL data()[164] 3.516s passed
seqDef_split data()[165] 3.380s passed
seqDef_induction_upper data()[166] 3.286s passed
seqDef_induction_upper_concrete data()[167] 3.485s passed
seqDef_induction_lower data()[168] 3.614s passed
seqDef_induction_lower_concrete data()[169] 3.741s passed
jdiv_one data()[16] 3.185s passed
seqDef_split_in_three data()[170] 3.706s passed
seqDef_empty data()[171] 3.643s passed
seqDef_one_summand data()[172] 3.615s passed
seqDef_lower_equals_upper data()[173] 3.575s passed
seqDefOfSeq data()[174] 3.742s passed
seqSelfDefinitionEQ2 data()[175] 3.583s passed
indexOfSeqSingleton data()[176] 3.574s passed
indexOfSeqConcatFirst data()[177] 3.721s passed
indexOfSeqConcatSecond data()[178] 3.635s passed
indexOfSeqSub data()[179] 3.571s passed
div_zero data()[17] 3.184s passed
lenOfArray2seq data()[180] 3.634s passed
getAnyOfArray2seq data()[181] 3.201s passed
getOfArray2seq data()[182] 3.095s passed
getAnyOfNPermInv data()[183] 3.090s passed
seqNPermRange data()[184] 3.186s passed
seqPermTrans data()[185] 3.204s passed
seqPermRefl data()[186] 3.123s passed
seqPermSplit data()[187] 3.086s passed
seqNPermRight data()[188] 3.306s passed
seqPermFromSwap data()[189] 3.135s passed
divResZero1 data()[18] 3.238s passed
seqPermTransAlt0 data()[190] 3.093s passed
seqPermTransAlt1 data()[191] 3.102s passed
seqPermTransAlt2 data()[192] 3.080s passed
seqPermTransAlt3 data()[193] 3.090s passed
seqPermForall data()[194] 3.179s passed
seqPermExists data()[195] 3.179s passed
schiffl_lemma_2 data()[196] 22.018s passed
schiffl_thm_1 data()[197] 3.870s passed
eqSameSeq data()[198] 3.286s passed
divResZero2 data()[19] 3.156s passed
eqTermCut data()[1] 3.653s passed
divResOne1 data()[20] 3.114s passed
divResOne2 data()[21] 3.136s passed
div_cancel1 data()[22] 3.142s passed
div_cancel2 data()[23] 3.100s passed
divAddMultDenom data()[24] 3.133s passed
divMinus data()[25] 3.149s passed
divMinusDenom data()[26] 3.116s passed
divLeastDPos data()[27] 3.140s passed
divLeastDNeg data()[28] 3.085s passed
divGreatestDPos data()[29] 3.099s passed
equivAllRight data()[2] 3.480s passed
divGreatestDNeg data()[30] 3.092s passed
divIncreasingPos data()[31] 3.076s passed
divIncreasingNeg data()[32] 3.101s passed
jdiv_zero data()[33] 3.093s passed
jdivPulloutMinusNum data()[34] 3.082s passed
jdivPulloutMinusDenom data()[35] 3.163s passed
jdiv_uniquePosPos data()[36] 3.094s passed
jdiv_uniquePosNeg data()[37] 3.121s passed
jdiv_uniqueNegPos data()[38] 3.092s passed
jdiv_uniqueNegNeg data()[39] 3.085s passed
irrflConcrete1 data()[3] 3.445s passed
jdivMultDenom1 data()[40] 3.133s passed
jdivMultDenom2 data()[41] 3.079s passed
mod_geZero data()[42] 3.098s passed
mod_lessDenom data()[43] 3.124s passed
jmod_NumPos data()[44] 3.085s passed
jmod_NumNeg data()[45] 3.118s passed
jmod_geZero data()[46] 3.088s passed
jmodNumZero data()[47] 3.118s passed
jmod_pulloutminusNum data()[48] 3.121s passed
jmod_pulloutminusDenom data()[49] 3.066s passed
irrflConcrete2 data()[4] 3.264s passed
jmodUnique1 data()[50] 3.129s passed
jmodUnique2 data()[51] 3.164s passed
intDivRem data()[52] 3.064s passed
jmodjmod data()[53] 3.130s passed
jmodDivisible data()[54] 3.095s passed
jmodDivisibleRep data()[55] 3.075s passed
jdivAddMultDenom data()[56] 3.217s passed
jmodAltZero data()[57] 3.085s passed
jmodAddMultDenomZero data()[58] 3.080s passed
polyDiv_zero data()[59] 3.065s passed
cancel_gtPos data()[5] 3.243s passed
polyMod_ltdivDenom data()[60] 3.069s passed
bsum_empty data()[61] 3.053s passed
bsum_induction_upper data()[62] 3.060s passed
bsum_induction_lower data()[63] 3.064s passed
bsum_num_of_bounds data()[64] 3.098s passed
bsum_num_of_bounds2 data()[65] 3.078s passed
bsum_induction_upper2 data()[66] 3.088s passed
bsum_induction_upper_concrete data()[67] 3.067s passed
bsum_induction_upper_concrete_2 data()[68] 3.058s passed
bsum_induction_upper2_concrete data()[69] 3.069s passed
cancel_gtNeg data()[6] 3.205s passed
bsum_induction_lower_concrete data()[70] 3.056s passed
bsum_induction_lower2 data()[71] 3.064s passed
bsum_induction_lower2_concrete data()[72] 3.079s passed
bsum_positive data()[73] 3.104s passed
bsum_upper_bound data()[74] 3.119s passed
bsum_lower_bound data()[75] 3.123s passed
bsum_positive_lower_bound_element data()[76] 3.102s passed
bsum_sub_same_index data()[77] 3.131s passed
bsum_less_same_index data()[78] 3.118s passed
bsum_equal_except_one_index data()[79] 3.093s passed
moduloIntIsInInt data()[7] 3.149s passed
bsum_num_of_is_max data()[80] 3.111s passed
bsum_num_of_is_max2 data()[81] 3.084s passed
bsum_num_of_is_max3 data()[82] 3.093s passed
bsum_num_of_is_max4 data()[83] 3.092s passed
bsum_num_of_lt_max data()[84] 3.071s passed
bsum_num_of_lt_max2 data()[85] 3.090s passed
bsum_num_of_lt_max3 data()[86] 3.082s passed
bsum_num_of_lt_max4 data()[87] 3.103s passed
bsum_num_of_gt0 data()[88] 3.080s passed
bsum_num_of_gt0_alt data()[89] 3.081s passed
moduloLongIsInLong data()[8] 3.158s passed
bsum_add_concrete data()[90] 3.100s passed
bprod_all_positive data()[91] 3.077s passed
bprod_split data()[92] 3.049s passed
powConcrete0 data()[93] 3.088s passed
powConcrete1 data()[94] 3.060s passed
powSplitFactor data()[95] 3.087s passed
powAdd data()[96] 3.070s passed
powMono data()[97] 3.067s passed
powMonoConcrete data()[98] 3.080s passed
powMonoConcreteRight data()[99] 3.060s passed
moduloShortIsInShort data()[9] 3.159s passed

Standard output

282        INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src/test/resources/testcase/dummyTrue.key 
304        DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 9.56ms 
506        INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
526        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)

1517       DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for Meta 
1519       DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for Meta 
1524       DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for Meta 
1524       DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for Meta 
3193       DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for JavaBigintExpression 
8320       DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 7.81s 
8384       INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof dummyTrue.key 
8417       DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 33.1ns 
8428       INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/firstOrder/Taclet_eqTermCut.proof 
8428       DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 327.7ns 
8431       INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
11152      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.72s 
11154      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: eqTermCut 
12052      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: eqTermCut 
12075      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 17.5ms 
12084      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/firstOrder/Taclet_equivAllRight.proof 
12084      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 234.7ns 
12085      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
14663      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.58s 
14663      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: equivAllRight 
15547      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: equivAllRight 
15561      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 10.66ms 
15564      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_irrflConcrete1.proof 
15564      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 224.3ns 
15566      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
18151      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.59s 
18152      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: irrflConcrete1 
18999      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: irrflConcrete1 
19006      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.87ms 
19008      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_irrflConcrete2.proof 
19009      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 292.2ns 
19010      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
21437      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.43s 
21437      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: irrflConcrete2 
22253      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: irrflConcrete2 
22269      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 11.77ms 
22273      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_cancel_gtPos.proof 
22274      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 948.71ns 
22275      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
24703      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.43s 
24703      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: cancel_gtPos 
25473      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: cancel_gtPos 
25513      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 36.14ms 
25516      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_cancel_gtNeg.proof 
25517      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 482.11ns 
25519      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
27922      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.4s 
27922      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: cancel_gtNeg 
28700      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: cancel_gtNeg 
28718      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 15.61ms 
28720      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intRulesIgnoringOF/Taclet_moduloIntIsInInt.proof 
28720      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 112.6ns 
28721      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
31086      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.37s 
31087      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: moduloIntIsInInt 
31864      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: moduloIntIsInInt 
31867      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 698.21ns 
31869      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intRulesIgnoringOF/Taclet_moduloLongIsInLong.proof 
31869      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 137.3ns 
31870      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
34239      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.37s 
34239      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: moduloLongIsInLong 
35022      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: moduloLongIsInLong 
35025      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 627.91ns 
35030      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intRulesIgnoringOF/Taclet_moduloShortIsInShort.proof 
35031      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 135.5ns 
35032      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
37393      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.36s 
37393      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: moduloShortIsInShort 
38184      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: moduloShortIsInShort 
38187      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 555.61ns 
38189      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intRulesIgnoringOF/Taclet_moduloByteIsInByte.proof 
38190      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 316.6ns 
38191      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
40572      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.38s 
40573      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: moduloByteIsInByte 
41324      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: moduloByteIsInByte 
41327      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 592.71ns 
41330      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intRulesIgnoringOF/Taclet_moduloCharIsInChar.proof 
41330      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 329.4ns 
41331      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
43701      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.37s 
43702      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: moduloCharIsInChar 
44471      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: moduloCharIsInChar 
44474      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 526.31ns 
44477      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_div_unique1.proof 
44477      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 338.1ns 
44478      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
46846      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.37s 
46847      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: div_unique1 
47631      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: div_unique1 
47672      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 36.63ms 
47677      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_div_unique2.proof 
47677      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 397ns 
47679      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
50046      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.37s 
50047      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: div_unique2 
50807      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: div_unique2 
50846      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 34.88ms 
50848      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_div_exists.proof 
50848      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 141.2ns 
50849      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
53207      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.36s 
53208      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: div_exists 
53985      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: div_exists 
54157      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 163.58ms 
54161      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_div_one.proof 
54161      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 154.1ns 
54162      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
56489      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.33s 
56489      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: div_one 
57259      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: div_one 
57263      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.51ms 
57264      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdiv_one.proof 
57265      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 85.7ns 
57265      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
59652      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.39s 
59652      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdiv_one 
60443      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdiv_one 
60448      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.12ms 
60451      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_div_zero.proof 
60451      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 302.6ns 
60452      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
62814      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.36s 
62814      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: div_zero 
63578      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: div_zero 
63631      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 48.97ms 
63636      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divResZero1.proof 
63636      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 351.6ns 
63637      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
66099      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.46s 
66100      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divResZero1 
66842      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divResZero1 
66871      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 18.63ms 
66873      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divResZero2.proof 
66874      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 335ns 
66876      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
69230      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.35s 
69230      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divResZero2 
70013      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divResZero2 
70026      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 10.56ms 
70029      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divResOne1.proof 
70029      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 351.2ns 
70031      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
72360      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.33s 
72361      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divResOne1 
73126      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divResOne1 
73141      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 12.31ms 
73144      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divResOne2.proof 
73144      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 313.5ns 
73145      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
75498      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.35s 
75499      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divResOne2 
76255      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divResOne2 
76277      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 17.8ms 
76284      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_div_cancel1.proof 
76286      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 2.29ms 
76287      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
78632      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.34s 
78632      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: div_cancel1 
79398      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: div_cancel1 
79423      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 21.87ms 
79424      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_div_cancel2.proof 
79425      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 129ns 
79425      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
81759      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.33s 
81759      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: div_cancel2 
82520      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: div_cancel2 
82523      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.12ms 
82524      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divAddMultDenom.proof 
82525      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 93ns 
82525      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
84858      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.33s 
84859      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divAddMultDenom 
85617      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divAddMultDenom 
85656      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 33.89ms 
85658      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divMinus.proof 
85658      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 119ns 
85659      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
87977      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.32s 
87977      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divMinus 
88737      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divMinus 
88805      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 60.82ms 
88806      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divMinusDenom.proof 
88807      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 189.3ns 
88808      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
91141      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.33s 
91141      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divMinusDenom 
91878      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divMinusDenom 
91921      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 37.42ms 
91923      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divLeastDPos.proof 
91923      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 118.8ns 
91924      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
94255      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.33s 
94255      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divLeastDPos 
95045      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divLeastDPos 
95059      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 10.87ms 
95064      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divLeastDNeg.proof 
95065      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 1.32ms 
95068      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
97376      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.31s 
97376      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divLeastDNeg 
98134      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divLeastDNeg 
98146      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 9.57ms 
98147      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divGreatestDPos.proof 
98147      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 102.4ns 
98148      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
100474     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.33s 
100474     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divGreatestDPos 
101234     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divGreatestDPos 
101245     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 8.22ms 
101246     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divGreatestDNeg.proof 
101246     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 84.3ns 
101247     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
103570     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.32s 
103570     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divGreatestDNeg 
104330     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divGreatestDNeg 
104338     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 5.47ms 
104339     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divIncreasingPos.proof 
104339     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 102.1ns 
104340     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
106648     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.31s 
106648     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divIncreasingPos 
107406     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divIncreasingPos 
107413     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 5.27ms 
107415     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divIncreasingNeg.proof 
107415     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 82.7ns 
107416     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
109748     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.33s 
109748     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divIncreasingNeg 
110507     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divIncreasingNeg 
110514     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.79ms 
110516     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdiv_zero.proof 
110516     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 121.4ns 
110516     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
112839     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.32s 
112840     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdiv_zero 
113604     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdiv_zero 
113608     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.42ms 
113609     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdivPulloutMinusNum.proof 
113609     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 96.5ns 
113610     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
115941     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.33s 
115941     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdivPulloutMinusNum 
116679     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdivPulloutMinusNum 
116689     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 8.17ms 
116690     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdivPulloutMinusDenom.proof 
116691     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 102.4ns 
116691     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
119037     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.35s 
119037     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdivPulloutMinusDenom 
119800     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdivPulloutMinusDenom 
119853     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 47.02ms 
119854     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdiv_uniquePosPos.proof 
119854     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 93.7ns 
119855     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
122170     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.32s 
122170     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdiv_uniquePosPos 
122928     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdiv_uniquePosPos 
122946     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 15.07ms 
122947     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdiv_uniquePosNeg.proof 
122947     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 91.9ns 
122948     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
125288     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.34s 
125288     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdiv_uniquePosNeg 
126048     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdiv_uniquePosNeg 
126068     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 16.29ms 
126069     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdiv_uniqueNegPos.proof 
126069     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 110.4ns 
126070     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
128384     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.31s 
128384     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdiv_uniqueNegPos 
129142     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdiv_uniqueNegPos 
129159     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 14.61ms 
129160     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdiv_uniqueNegNeg.proof 
129161     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 95.9ns 
129161     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
131468     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.31s 
131469     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdiv_uniqueNegNeg 
132227     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdiv_uniqueNegNeg 
132244     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 14.48ms 
132245     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdivMultDenom1.proof 
132245     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 101.3ns 
132246     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
134575     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.33s 
134576     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdivMultDenom1 
135334     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdivMultDenom1 
135376     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 37.32ms 
135379     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdivMultDenom2.proof 
135379     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 299.8ns 
135380     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
137694     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.31s 
137695     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdivMultDenom2 
138453     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdivMultDenom2 
138456     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.13ms 
138458     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_mod_geZero.proof 
138458     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 293.5ns 
138459     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
140813     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.35s 
140813     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: mod_geZero 
141550     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: mod_geZero 
141554     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.51ms 
141555     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_mod_lessDenom.proof 
141555     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 87ns 
141556     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
143908     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.35s 
143908     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: mod_lessDenom 
144670     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: mod_lessDenom 
144679     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 6.21ms 
144680     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmod_NumPos.proof 
144680     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 76.4ns 
144681     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
146998     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.32s 
146998     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmod_NumPos 
147755     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmod_NumPos 
147763     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 6.37ms 
147764     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmod_NumNeg.proof 
147764     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 81.8ns 
147765     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
150098     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.33s 
150099     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmod_NumNeg 
150859     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmod_NumNeg 
150881     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 18.55ms 
150883     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmod_geZero.proof 
150883     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 302.6ns 
150884     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
153203     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.32s 
153204     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmod_geZero 
153962     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmod_geZero 
153970     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 6.07ms 
153971     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmodNumZero.proof 
153971     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 87.4ns 
153972     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
156273     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.3s 
156273     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmodNumZero 
157082     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmodNumZero 
157086     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.33ms 
157090     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmod_pulloutminusNum.proof 
157090     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 269.4ns 
157091     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
159443     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.35s 
159443     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmod_pulloutminusNum 
160203     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmod_pulloutminusNum 
160208     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.77ms 
160210     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmod_pulloutminusDenom.proof 
160210     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 276.2ns 
160211     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
162513     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.3s 
162514     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmod_pulloutminusDenom 
163270     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmod_pulloutminusDenom 
163274     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.16ms 
163276     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmodUnique1.proof 
163277     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 250.6ns 
163278     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
165600     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.32s 
165600     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmodUnique1 
166333     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmodUnique1 
166403     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 61.48ms 
166405     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmodUnique2.proof 
166405     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 103.3ns 
166406     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
168728     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.32s 
168728     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmodUnique2 
169488     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmodUnique2 
169567     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 69.95ms 
169568     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_intDivRem.proof 
169568     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 161.8ns 
169569     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
171866     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.3s 
171866     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: intDivRem 
172628     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: intDivRem 
172631     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.48ms 
172632     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmodjmod.proof 
172632     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 90.2ns 
172633     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
174948     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.31s 
174948     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmodjmod 
175705     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmodjmod 
175760     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 50.32ms 
175763     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmodDivisible.proof 
175769     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 6.02ms 
175769     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
178072     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.3s 
178072     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmodDivisible 
178827     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmodDivisible 
178856     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 26.32ms 
178858     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmodDivisibleRep.proof 
178858     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 88.7ns 
178858     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
181196     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.34s 
181196     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmodDivisibleRep 
181929     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmodDivisibleRep 
181932     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.17ms 
181933     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdivAddMultDenom.proof 
181933     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 62.9ns 
181934     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
184250     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.32s 
184250     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdivAddMultDenom 
185004     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdivAddMultDenom 
185148     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 132.59ms 
185150     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmodAltZero.proof 
185150     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 142.5ns 
185151     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
187452     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.3s 
187452     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmodAltZero 
188220     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmodAltZero 
188233     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 11.24ms 
188235     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmodAddMultDenomZero.proof 
188235     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 76.8ns 
188237     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
190555     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.32s 
190555     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmodAddMultDenomZero 
191305     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmodAddMultDenomZero 
191313     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 6.19ms 
191314     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_polyDiv_zero.proof 
191315     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 73.6ns 
191315     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
193609     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.29s 
193609     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: polyDiv_zero 
194362     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: polyDiv_zero 
194378     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 14ms 
194380     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_polyMod_ltdivDenom.proof 
194380     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 82.7ns 
194380     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
196683     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.3s 
196704     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: polyMod_ltdivDenom 
197435     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: polyMod_ltdivDenom 
197447     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 6.12ms 
197449     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_empty.proof 
197449     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 81.9ns 
197449     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
199749     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.3s 
199750     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_empty 
200497     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_empty 
200501     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.69ms 
200502     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_induction_upper.proof 
200502     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 65.6ns 
200503     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
202797     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.29s 
202798     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_upper 
203556     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_induction_upper 
203561     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.57ms 
203562     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_induction_lower.proof 
203562     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 64.7ns 
203563     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
205872     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.31s 
205872     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_lower 
206602     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_induction_lower 
206625     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 19.6ms 
206626     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_bounds.proof 
206626     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 75.6ns 
206627     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
208942     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.32s 
208942     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_bounds 
209703     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_bounds 
209722     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 16.25ms 
209724     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_bounds2.proof 
209725     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 244.6ns 
209726     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
212029     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.3s 
212029     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_bounds2 
212785     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_bounds2 
212801     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 13.15ms 
212803     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_induction_upper2.proof 
212803     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 223ns 
212804     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
215130     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.33s 
215130     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_upper2 
215886     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_induction_upper2 
215890     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.57ms 
215891     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_induction_upper_concrete.proof 
215891     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 67.9ns 
215891     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
218192     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.3s 
218192     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_upper_concrete 
218953     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_induction_upper_concrete 
218957     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.6ms 
218958     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_induction_upper_concrete_2.proof 
218958     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 64.1ns 
218959     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
221256     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.3s 
221256     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_upper_concrete_2 
222009     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_induction_upper_concrete_2 
222014     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.67ms 
222015     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_induction_upper2_concrete.proof 
222015     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 68.5ns 
222016     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
224327     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.31s 
224328     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_upper2_concrete 
225080     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_induction_upper2_concrete 
225083     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.35ms 
225084     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_induction_lower_concrete.proof 
225084     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 71.4ns 
225085     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
227384     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.3s 
227384     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_lower_concrete 
228138     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_induction_lower_concrete 
228140     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 728.91ns 
228141     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_induction_lower2.proof 
228141     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 59.3ns 
228142     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
230465     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.32s 
230465     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_lower2 
231199     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_induction_lower2 
231204     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.29ms 
231206     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_induction_lower2_concrete.proof 
231206     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 316.1ns 
231207     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
233527     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.32s 
233527     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_lower2_concrete 
234280     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_induction_lower2_concrete 
234282     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.01ms 
234283     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_positive.proof 
234283     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 51.4ns 
234284     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
236583     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.3s 
236583     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_positive 
237335     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_positive 
237386     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 48.19ms 
237388     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_upper_bound.proof 
237389     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 219.9ns 
237390     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
239735     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.34s 
239735     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_upper_bound 
240467     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_upper_bound 
240505     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 35.6ms 
240508     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_lower_bound.proof 
240508     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 436.5ns 
240509     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
242837     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.33s 
242838     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_lower_bound 
243597     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_lower_bound 
243629     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 29.1ms 
243631     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_positive_lower_bound_element.proof 
243631     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 85.4ns 
243632     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
245932     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.3s 
245932     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_positive_lower_bound_element 
246689     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_positive_lower_bound_element 
246732     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 38.48ms 
246733     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_sub_same_index.proof 
246733     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 69.1ns 
246734     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
249076     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.34s 
249076     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_sub_same_index 
249833     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_sub_same_index 
249862     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 26.62ms 
249864     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_less_same_index.proof 
249864     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 81.6ns 
249864     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
252168     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.3s 
252168     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_less_same_index 
252926     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_less_same_index 
252979     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 48.69ms 
252982     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_equal_except_one_index.proof 
252982     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 221.4ns 
252983     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
255314     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.33s 
255314     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_equal_except_one_index 
256047     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_equal_except_one_index 
256073     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 23.46ms 
256075     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_is_max.proof 
256075     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 71.9ns 
256076     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
258408     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.33s 
258408     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_is_max 
259165     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_is_max 
259185     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 16.96ms 
259186     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_is_max2.proof 
259186     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 83ns 
259187     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
261487     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.3s 
261487     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_is_max2 
262244     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_is_max2 
262268     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 21.1ms 
262270     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_is_max3.proof 
262271     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 207.1ns 
262272     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
264589     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.32s 
264589     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_is_max3 
265342     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_is_max3 
265361     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 16.83ms 
265362     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_is_max4.proof 
265363     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 68.7ns 
265363     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
267672     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.31s 
267673     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_is_max4 
268425     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_is_max4 
268454     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 25.59ms 
268455     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_lt_max.proof 
268455     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 82.9ns 
268456     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
270769     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.31s 
270769     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_lt_max 
271499     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_lt_max 
271524     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 22.11ms 
271525     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_lt_max2.proof 
271525     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 84.5ns 
271526     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
273836     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.31s 
273836     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_lt_max2 
274589     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_lt_max2 
274615     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 22.48ms 
274616     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_lt_max3.proof 
274616     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 84.1ns 
274617     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
276917     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.3s 
276917     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_lt_max3 
277671     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_lt_max3 
277696     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 21.86ms 
277697     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_lt_max4.proof 
277697     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 86.6ns 
277698     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
280013     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.32s 
280013     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_lt_max4 
280745     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_lt_max4 
280799     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 51.88ms 
280801     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_gt0.proof 
280801     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 70.2ns 
280802     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
283099     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.3s 
283099     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_gt0 
283853     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_gt0 
283879     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 23.2ms 
283880     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_gt0_alt.proof 
283880     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 73.8ns 
283881     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
286178     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.3s 
286178     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_gt0_alt 
286934     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_gt0_alt 
286961     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 23.78ms 
286962     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_add_concrete.proof 
286962     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 70.6ns 
286963     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
289298     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.34s 
289298     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_add_concrete 
290053     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_add_concrete 
290060     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 5.85ms 
290062     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bprod/Taclet_bprod_all_positive.proof 
290062     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 60.4ns 
290062     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
292363     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.3s 
292363     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bprod_all_positive 
293120     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bprod_all_positive 
293138     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 14.67ms 
293139     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bprod/Taclet_bprod_split.proof 
293139     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 49ns 
293140     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
295451     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.31s 
295451     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bprod_split 
296183     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bprod_split 
296187     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.03ms 
296188     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powConcrete0.proof 
296188     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 64.3ns 
296188     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
298514     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.33s 
298514     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powConcrete0 
299272     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powConcrete0 
299274     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 670.41ns 
299275     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powConcrete1.proof 
299275     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 59.1ns 
299276     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
301575     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.3s 
301575     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powConcrete1 
302332     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powConcrete1 
302334     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 746.81ns 
302336     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powSplitFactor.proof 
302336     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 54.7ns 
302336     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
304654     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.32s 
304655     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powSplitFactor 
305414     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powSplitFactor 
305422     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.91ms 
305423     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powAdd.proof 
305423     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 64.5ns 
305424     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
307727     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.3s 
307727     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powAdd 
308486     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powAdd 
308492     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.42ms 
308493     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powMono.proof 
308493     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 64.1ns 
308494     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
310791     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.3s 
310791     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powMono 
311546     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powMono 
311559     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 10.08ms 
311560     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powMonoConcrete.proof 
311560     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 63ns 
311561     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
313879     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.32s 
313879     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powMonoConcrete 
314635     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powMonoConcrete 
314639     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.91ms 
314640     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powMonoConcreteRight.proof 
314640     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 52.3ns 
314641     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
316941     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.3s 
316941     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powMonoConcreteRight 
317697     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powMonoConcreteRight 
317699     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 534.3ns 
317700     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powPositive.proof 
317700     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 61.8ns 
317701     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
320018     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.32s 
320019     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powPositive 
320754     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powPositive 
320762     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 5.71ms 
320764     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powPositiveConcrete.proof 
320764     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 187.6ns 
320765     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
323074     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.31s 
323075     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powPositiveConcrete 
323829     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powPositiveConcrete 
323831     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 664.91ns 
323832     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powGeq1Concrete.proof 
323832     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 52.8ns 
323833     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
326127     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.29s 
326127     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powGeq1Concrete 
326882     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powGeq1Concrete 
326884     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 571.91ns 
326885     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_pow2InIntLower.proof 
326885     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 69.5ns 
326886     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
329198     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.31s 
329198     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: pow2InIntLower 
329929     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: pow2InIntLower 
329931     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 583.41ns 
329932     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_pow2InIntUpper.proof 
329932     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 65ns 
329933     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
332240     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.31s 
332241     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: pow2InIntUpper 
332993     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: pow2InIntUpper 
332997     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.09ms 
332998     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logSelfConcrete.proof 
332998     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 60.3ns 
332998     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
335293     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.29s 
335293     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logSelfConcrete 
336047     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logSelfConcrete 
336056     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 6.89ms 
336057     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_log1Concrete.proof 
336057     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 60.9ns 
336057     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
338364     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.31s 
338364     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: log1Concrete 
339121     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: log1Concrete 
339126     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.64ms 
339128     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logProduct.proof 
339129     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 207.1ns 
339136     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
341445     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.31s 
341446     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logProduct 
342202     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logProduct 
342209     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.93ms 
342210     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logTimesBaseConcrete.proof 
342210     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 51.7ns 
342211     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
344524     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.31s 
344524     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logTimesBaseConcrete 
345256     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logTimesBaseConcrete 
345260     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.18ms 
345261     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logProdIdentity.proof 
345261     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 51.8ns 
345262     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
347572     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.31s 
347572     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logProdIdentity 
348327     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logProdIdentity 
348343     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 12.9ms 
348344     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logProdIdentityConcrete.proof 
348344     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 69.4ns 
348345     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
350635     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.29s 
350635     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logProdIdentityConcrete 
351389     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logProdIdentityConcrete 
351392     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.81ms 
351394     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logPowIdentity.proof 
351394     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 56.2ns 
351394     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
353704     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.31s 
353704     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logPowIdentity 
354459     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logPowIdentity 
354462     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.29ms 
354463     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logPowIdentityConcrete.proof 
354463     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 51.2ns 
354464     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
356756     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.29s 
356756     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logPowIdentityConcrete 
357511     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logPowIdentityConcrete 
357515     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.11ms 
357516     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logPositive.proof 
357516     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 50.6ns 
357517     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
359826     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.31s 
359826     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logPositive 
360577     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logPositive 
360594     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 14.12ms 
360595     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logPositiveConcrete.proof 
360595     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 62.7ns 
360595     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
362887     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.29s 
362888     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logPositiveConcrete 
363641     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logPositiveConcrete 
363645     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 494.71ns 
363646     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logMono.proof 
363646     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 60.3ns 
363647     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
365954     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.31s 
365954     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logMono 
366705     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logMono 
366743     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 34.48ms 
366745     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logMonoConcrete.proof 
366745     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 55.1ns 
366745     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
369045     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.3s 
369045     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logMonoConcrete 
369801     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logMonoConcrete 
369804     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.61ms 
369806     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powLogLess.proof 
369807     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 64ns 
369807     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
372125     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.32s 
372125     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powLogLess 
372886     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powLogLess 
372910     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 21.06ms 
372912     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powLogMore2.proof 
372912     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 69.3ns 
372913     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
375219     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.31s 
375219     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powLogMore2 
375973     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powLogMore2 
375993     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 17.89ms 
375995     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logLessThanPow.proof 
375995     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 66.8ns 
375995     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
378313     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.32s 
378313     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logLessThanPow 
379074     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logLessThanPow 
379098     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 21.71ms 
379100     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logLessThanPowConcrete.proof 
379100     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 71.2ns 
379100     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
381402     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.3s 
381402     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logLessThanPowConcrete 
382158     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logLessThanPowConcrete 
382160     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 520.5ns 
382162     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logSqueeze.proof 
382162     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 54.5ns 
382162     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
384482     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.32s 
384482     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logSqueeze 
385234     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logSqueeze 
385239     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.73ms 
385241     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/booleanRules/Taclet_ifthenelse_equals.proof 
385241     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 119.4ns 
385242     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
387534     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.29s 
387534     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: ifthenelse_equals 
388293     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: ifthenelse_equals 
388296     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.4ms 
388298     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/booleanRules/Taclet_ifthenelse_equals_1.proof 
388298     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 78.1ns 
388298     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
390615     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.32s 
390616     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: ifthenelse_equals_1 
391375     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: ifthenelse_equals_1 
391377     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 854.31ns 
391379     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/booleanRules/Taclet_ifthenelse_equals_2.proof 
391379     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 183.6ns 
391380     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
393688     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.31s 
393689     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: ifthenelse_equals_2 
394427     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: ifthenelse_equals_2 
394429     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 861.71ns 
394431     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/locSet/Taclet_disjointWithSingleton1.proof 
394431     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 50.1ns 
394431     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
396741     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.31s 
396741     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: disjointWithSingleton1 
397499     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: disjointWithSingleton1 
397502     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.39ms 
397503     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/locSet/Taclet_disjointWithSingleton2.proof 
397503     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 48.5ns 
397504     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
399814     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.31s 
399814     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: disjointWithSingleton2 
400572     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: disjointWithSingleton2 
400575     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.21ms 
400576     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/locSet/Taclet_disjointArrayRanges.proof 
400576     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 65.9ns 
400577     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
402880     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.3s 
402880     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: disjointArrayRanges 
403644     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: disjointArrayRanges 
403660     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 7.61ms 
403661     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/locSet/Taclet_disjointArrayRangeAllFields1.proof 
403661     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 84.8ns 
403662     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
405978     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.32s 
405978     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: disjointArrayRangeAllFields1 
406739     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: disjointArrayRangeAllFields1 
406751     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 9.82ms 
406752     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/locSet/Taclet_disjointArrayRangeAllFields2.proof 
406752     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 67.7ns 
406753     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
409064     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.31s 
409064     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: disjointArrayRangeAllFields2 
409827     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: disjointArrayRangeAllFields2 
409837     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 9.03ms 
409839     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqSelfDefinition.proof 
409839     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 60.8ns 
409839     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
412136     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.3s 
412136     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqSelfDefinition 
412903     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqSelfDefinition 
412915     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 10.39ms 
412917     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqOutsideValue.proof 
412917     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 68.4ns 
412917     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
415234     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.32s 
415234     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqOutsideValue 
416003     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqOutsideValue 
416007     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.68ms 
416009     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_castedGetAny.proof 
416009     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 71.3ns 
416009     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
418329     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.32s 
418329     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: castedGetAny 
419095     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: castedGetAny 
419106     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 9.44ms 
419107     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqGetAlphaCast.proof 
419107     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 63.8ns 
419108     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
421410     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.3s 
421410     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqGetAlphaCast 
422177     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqGetAlphaCast 
422179     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 738.51ns 
422180     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqSingleton.proof 
422180     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 60.3ns 
422181     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
424498     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.32s 
424498     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqSingleton 
425265     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqSingleton 
425268     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.37ms 
425269     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqSingletonConcrete.proof 
425269     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 61.4ns 
425270     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
427595     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.32s 
427595     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqSingletonConcrete 
428364     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqSingletonConcrete 
428366     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 821.91ns 
428367     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqConcat.proof 
428367     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 61.3ns 
428368     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
430683     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.31s 
430683     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqConcat 
431427     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqConcat 
431439     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 9.28ms 
431440     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqSub.proof 
431440     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 65.1ns 
431441     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
433764     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.32s 
433764     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqSub 
434530     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqSub 
434534     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.7ms 
434535     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqReverse.proof 
434535     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 65.9ns 
434536     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
436856     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.32s 
436856     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqReverse 
437624     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqReverse 
437631     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.96ms 
437633     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqEmpty.proof 
437633     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 185.8ns 
437634     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
439954     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.32s 
439955     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqEmpty 
440724     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqEmpty 
440727     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 808.11ns 
440728     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqSingleton.proof 
440728     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 58.7ns 
440728     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
443063     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.33s 
443063     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqSingleton 
443814     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqSingleton 
443816     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 646ns 
443817     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqConcat.proof 
443817     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 61.4ns 
443818     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
446148     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.33s 
446148     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqConcat 
446918     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqConcat 
446922     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.24ms 
446923     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqSub.proof 
446924     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 72.4ns 
446924     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
449248     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.32s 
449248     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqSub 
450017     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqSub 
450020     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.42ms 
450021     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqReverse.proof 
450021     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 82.9ns 
450022     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
452352     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.33s 
452352     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqReverse 
453121     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqReverse 
453124     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.51ms 
453125     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_equalityToSeqGetAndSeqLenLeft.proof 
453125     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 79.9ns 
453126     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
455457     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.33s 
455457     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: equalityToSeqGetAndSeqLenLeft 
456226     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: equalityToSeqGetAndSeqLenLeft 
456228     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.27ms 
456230     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_equalityToSeqGetAndSeqLenRight.proof 
456230     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 58.9ns 
456230     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
458553     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.32s 
458553     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: equalityToSeqGetAndSeqLenRight 
459304     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: equalityToSeqGetAndSeqLenRight 
459310     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.73ms 
459312     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqSingletonEQ.proof 
459312     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 55.7ns 
459312     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
461644     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.33s 
461644     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqSingletonEQ 
462410     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqSingletonEQ 
462413     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.32ms 
462414     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqConcatEQ.proof 
462414     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 59.2ns 
462415     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
464737     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.32s 
464737     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqConcatEQ 
465504     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqConcatEQ 
465515     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 8.8ms 
465516     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqSubEQ.proof 
465516     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 67.8ns 
465517     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
468073     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.56s 
468073     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqSubEQ 
468931     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqSubEQ 
468933     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 704.61ns 
468935     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqReverseEQ.proof 
468935     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 62.3ns 
468935     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
471520     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.58s 
471520     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqReverseEQ 
472391     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqReverseEQ 
472398     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 5.27ms 
472399     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqEmptyEQ.proof 
472399     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 58.4ns 
472400     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
475132     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.73s 
475132     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqEmptyEQ 
476082     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqEmptyEQ 
476085     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 874.41ns 
476086     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqSingletonEQ.proof 
476086     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 48.7ns 
476086     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
478590     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.5s 
478590     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqSingletonEQ 
479536     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqSingletonEQ 
479539     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 779.31ns 
479540     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqConcatEQ.proof 
479540     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 72.1ns 
479540     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
482388     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.85s 
482388     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqConcatEQ 
483177     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqConcatEQ 
483181     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.14ms 
483183     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqSubEQ.proof 
483183     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 49.2ns 
483183     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
485971     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.79s 
485971     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqSubEQ 
486776     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqSubEQ 
486779     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.5ms 
486780     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqReverseEQ.proof 
486780     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 49.5ns 
486781     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
489460     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.68s 
489460     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqReverseEQ 
490340     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqReverseEQ 
490343     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.96ms 
490344     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqDefEQ.proof 
490344     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 71.9ns 
490345     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
493132     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.79s 
493133     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqDefEQ 
493936     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqDefEQ 
493940     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.13ms 
493942     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqDefEQ.proof 
493943     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 186.9ns 
493943     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
496621     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.68s 
496621     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqDefEQ 
497472     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqDefEQ 
497477     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.25ms 
497478     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqConcatWithSeqEmpty1.proof 
497478     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 63.7ns 
497479     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
500261     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.78s 
500261     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqConcatWithSeqEmpty1 
501107     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqConcatWithSeqEmpty1 
501122     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 12.58ms 
501123     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqConcatWithSeqEmpty2.proof 
501123     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 51.4ns 
501124     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
503912     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.79s 
503912     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqConcatWithSeqEmpty2 
504868     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqConcatWithSeqEmpty2 
504884     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 13.83ms 
504885     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqReverseOfSeqEmpty.proof 
504885     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 64.8ns 
504886     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
507566     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.68s 
507566     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqReverseOfSeqEmpty 
508478     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqReverseOfSeqEmpty 
508489     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 8.7ms 
508490     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_subSeqComplete.proof 
508490     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 53.8ns 
508491     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
511216     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.73s 
511217     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: subSeqComplete 
512165     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: subSeqComplete 
512176     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 8.94ms 
512177     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_subSeqTailR.proof 
512177     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 69ns 
512178     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
514915     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.74s 
514915     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: subSeqTailR 
515814     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: subSeqTailR 
515842     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 25.68ms 
515843     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_subSeqTailL.proof 
515844     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 54.3ns 
515844     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
518540     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.7s 
518541     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: subSeqTailL 
519309     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: subSeqTailL 
519335     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 24.11ms 
519336     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_subSeqTailEQR.proof 
519336     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 65.5ns 
519337     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
522091     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.75s 
522091     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: subSeqTailEQR 
522959     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: subSeqTailEQR 
522983     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 21.87ms 
522985     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_subSeqTailEQL.proof 
522985     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 60.5ns 
522985     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
525662     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.68s 
525662     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: subSeqTailEQL 
526485     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: subSeqTailEQL 
526500     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 12.56ms 
526501     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDef_split.proof 
526501     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 65.1ns 
526502     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
528980     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.48s 
528980     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_split 
529849     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDef_split 
529880     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 26.99ms 
529881     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDef_induction_upper.proof 
529881     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 55.6ns 
529882     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
532343     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.46s 
532343     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_induction_upper 
533117     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDef_induction_upper 
533165     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 44.36ms 
533166     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDef_induction_upper_concrete.proof 
533166     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 68.2ns 
533167     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
535766     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.6s 
535766     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_induction_upper_concrete 
536612     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDef_induction_upper_concrete 
536651     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 35.3ms 
536652     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDef_induction_lower.proof 
536652     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 63.3ns 
536653     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
539311     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.66s 
539312     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_induction_lower 
540221     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDef_induction_lower 
540263     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 38.87ms 
540266     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDef_induction_lower_concrete.proof 
540266     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 70.3ns 
540266     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
543033     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.77s 
543033     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_induction_lower_concrete 
543887     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDef_induction_lower_concrete 
543990     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 99.98ms 
544028     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDef_split_in_three.proof 
544031     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 2.16ms 
544039     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
546732     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.69s 
546732     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_split_in_three 
547606     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDef_split_in_three 
547726     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 113.1ms 
547727     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDef_empty.proof 
547727     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 70.9ns 
547728     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
550575     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.85s 
550575     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_empty 
551362     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDef_empty 
551369     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 6.02ms 
551371     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDef_one_summand.proof 
551371     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 57.7ns 
551372     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
553959     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.59s 
553959     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_one_summand 
554975     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDef_one_summand 
554984     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 7.58ms 
554986     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDef_lower_equals_upper.proof 
554986     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 68.2ns 
554986     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
557704     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.72s 
557704     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_lower_equals_upper 
558554     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDef_lower_equals_upper 
558560     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.8ms 
558561     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDefOfSeq.proof 
558561     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 77.6ns 
558562     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
561307     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.75s 
561307     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDefOfSeq 
562284     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDefOfSeq 
562302     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 15.01ms 
562303     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqSelfDefinitionEQ2.proof 
562303     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 62.3ns 
562304     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
565011     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.71s 
565011     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqSelfDefinitionEQ2 
565873     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqSelfDefinitionEQ2 
565884     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 8.85ms 
565885     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_indexOfSeqSingleton.proof 
565885     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 57.3ns 
565886     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
568654     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.77s 
568654     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: indexOfSeqSingleton 
569455     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: indexOfSeqSingleton 
569458     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.68ms 
569469     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_indexOfSeqConcatFirst.proof 
569470     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 1.12ms 
569483     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
572224     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.74s 
572224     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: indexOfSeqConcatFirst 
573167     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: indexOfSeqConcatFirst 
573184     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 14.94ms 
573185     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_indexOfSeqConcatSecond.proof 
573186     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 70.1ns 
573186     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
575918     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.73s 
575918     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: indexOfSeqConcatSecond 
576803     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: indexOfSeqConcatSecond 
576819     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 14.02ms 
576820     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_indexOfSeqSub.proof 
576820     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 78.3ns 
576821     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
579405     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.58s 
579406     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: indexOfSeqSub 
580371     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: indexOfSeqSub 
580390     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 16.85ms 
580392     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfArray2seq.proof 
580392     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 67.6ns 
580392     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
582998     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.61s 
582998     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfArray2seq 
584021     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfArray2seq 
584024     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.14ms 
584025     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getAnyOfArray2seq.proof 
584025     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 46.8ns 
584026     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
586455     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.43s 
586455     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getAnyOfArray2seq 
587222     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getAnyOfArray2seq 
587226     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.15ms 
587227     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfArray2seq.proof 
587227     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 63.2ns 
587227     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
589546     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.32s 
589546     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfArray2seq 
590314     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfArray2seq 
590320     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.62ms 
590321     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_getAnyOfNPermInv.proof 
590322     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 64.7ns 
590322     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
592634     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.31s 
592635     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getAnyOfNPermInv 
593402     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getAnyOfNPermInv 
593409     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.31ms 
593412     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqNPermRange.proof 
593413     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 250.1ns 
593414     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
595758     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.34s 
595758     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqNPermRange 
596527     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqNPermRange 
596596     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 63.7ms 
596598     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermTrans.proof 
596598     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 67.8ns 
596598     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
599000     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.4s 
599000     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermTrans 
599773     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermTrans 
599801     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 24.05ms 
599802     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermRefl.proof 
599802     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 65.5ns 
599803     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
602135     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.33s 
602135     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermRefl 
602901     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermRefl 
602923     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 20.01ms 
602925     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermSplit.proof 
602925     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 62.1ns 
602925     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
605234     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.31s 
605234     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermSplit 
606007     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermSplit 
606009     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 297ns 
606011     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqNPermRight.proof 
606011     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 67.6ns 
606012     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
608352     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.34s 
608352     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqNPermRight 
609119     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqNPermRight 
609314     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 184.5ms 
609317     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermFromSwap.proof 
609317     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 194ns 
609318     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
611632     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.31s 
611632     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermFromSwap 
612401     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermFromSwap 
612451     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 44.81ms 
612453     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermTransAlt0.proof 
612453     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 76.8ns 
612454     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
614775     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.32s 
614775     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermTransAlt0 
615542     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermTransAlt0 
615544     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 333.9ns 
615546     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermTransAlt1.proof 
615546     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 51.5ns 
615546     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
617857     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.31s 
617857     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermTransAlt1 
618644     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermTransAlt1 
618646     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 334ns 
618647     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermTransAlt2.proof 
618647     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 61.4ns 
618648     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
620956     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.31s 
620956     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermTransAlt2 
621725     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermTransAlt2 
621727     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 348.8ns 
621728     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermTransAlt3.proof 
621728     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 51.7ns 
621729     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
624050     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.32s 
624050     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermTransAlt3 
624815     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermTransAlt3 
624817     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 466.81ns 
624818     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermForall.proof 
624818     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 60.7ns 
624819     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
627125     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.31s 
627125     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermForall 
627892     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermForall 
627982     INFO  Test worker     d.u.i.k.s.SMTFocusResults Analyzing unsat core: (L_1 L_3 L_4) 
627995     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 100.66ms 
627997     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermExists.proof 
627997     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 55.8ns 
627998     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
630354     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.36s 
630354     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermExists 
631122     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermExists 
631174     INFO  Test worker     d.u.i.k.s.SMTFocusResults Analyzing unsat core: (L_1 L_3 L_5 L_6 L_7) 
631175     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 50.94ms 
631176     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm2/Taclet_schiffl_lemma_2.proof 
631176     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 76.8ns 
631178     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
633502     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.32s 
633503     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: schiffl_lemma_2 
634305     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: schiffl_lemma_2 
634306     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.2ns 
634334     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 1: 'macro split-prop' 
634382     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 2: 'rule allRight' 
634406     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 3: 'rule allRight' 
634414     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 4: 'macro split-prop' 
634423     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 5: 'rule 'seqPermDefLeft'' 
634426     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 6: 'rule 'andLeft'' 
634427     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 7: 'rule 'exLeft'' 
634430     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 8: 'macro split-prop' 
634433     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 9: 'rule  seqNPermRange' 
634435     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 10: 'instantiate var=iv with='v_x_0' occ=1' 
634440     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 11: 'rule impLeft' 
634441     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 12: 'tryclose branch' 
634624     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 13: 'rule andLeft' 
634625     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 14: 'rule andLeft' 
634626     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 15: 'instantiate var=iv with='v_y_0' occ=1' 
634627     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 16: 'rule impLeft' 
634628     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 17: 'tryclose branch' 
634745     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 18: 'rule andLeft' 
634746     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 19: 'rule andLeft' 
634747     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 20: 'rule seqNPermDefLeft' 
634749     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 21: 'instantiate var=iv with='v_x_0' occ=2' 
634750     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 22: 'rule impLeft' 
634751     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 23: 'tryclose branch' 
634900     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 24: 'rule exLeft' 
634901     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 25: 'rule andLeft' 
634903     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 26: 'rule andLeft' 
634903     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 27: 'instantiate hide var=iv with='v_y_0' occ=2' 
634904     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 28: 'rule impLeft' 
634905     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 29: 'tryclose branch' 
635009     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 30: 'rule exLeft' 
635011     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 31: 'rule andLeft' 
635012     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 32: 'rule andLeft' 
635013     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 33: 'instantiate var=iv with='jv_0' occ=1' 
635014     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 34: 'rule impLeft' 
635015     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 35: 'tryclose branch' 
635020     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 36: 'rule andLeft' 
635021     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 37: 'rule andLeft' 
635022     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 38: 'rule castAdd formula='s_0[jv_0] = v_x_0' occ=0' 
635024     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 39: 'instantiate hide var=iv with='jv_1' occ=1' 
635025     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 40: 'rule impLeft' 
635026     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 41: 'tryclose branch' 
635032     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 42: 'rule andLeft' 
635032     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 43: 'rule andLeft' 
635033     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 44: 'rule castAdd formula='s_0[jv_1] = v_y_0' occ=0' 
635034     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 45: 'instantiate var=iv  with='v_x_0'' 
635035     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 46: 'rule impLeft' 
635036     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 47: 'tryclose branch' 
635156     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 48: 'instantiate var=iv  with='v_y_0'' 
635158     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 49: 'rule impLeft' 
635159     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 50: 'tryclose branch' 
635264     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 51: 'cut 'v_x_0 = v_y_0'' 
635265     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)'' 
635268     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 53: 'rule andRight' 
635269     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 54: 'rule andRight' 
635270     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 55: 'rule andRight' 
635271     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 56: 'rule andRight' 
635272     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 57: 'rule lenOfSwap' 
635272     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 58: 'tryclose branch' 
635278     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 59: 'rule seqNPermSwapNPerm' 
635281     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 60: 'instantiate hide var='iv' with='v_x_0' occ=1' 
635282     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 61: 'instantiate hide var='jv' with='jv_0'' 
635283     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 62: 'rule impLeft' 
635283     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 63: 'tryclose branch' 
635382     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 64: 'tryclose branch' 
635385     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 65: 'rule allRight' 
635387     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 66: 'rule impRight' 
635388     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 67: 'rule andLeft' 
635389     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 68: 'instantiate var=iv with='v_iv_0'' 
635389     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 69: 'rule impLeft' 
635390     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 70: 'tryclose branch' 
635492     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 71: 'rule getOfSwap' 
635494     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 72: 'rule ifthenelse_negated' 
635495     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 73: 'rule ifthenelse_split occ=0' 
635497     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 74: 'rule andLeft' 
635497     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 75: 'rule andLeft' 
635498     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 76: 'rule andLeft' 
635498     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 77: 'rule ifthenelse_split occ=0' 
635500     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 78: 'tryclose branch' 
635583     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 79: 'rule ifthenelse_split occ=0' 
635585     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 80: 'tryclose branch' 
635681     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 81: 'tryclose branch' 
635685     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 82: 'tryclose branch' 
635689     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 83: 'rule getOfSwap' 
635690     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 84: 'rule ifthenelse_negated' 
635691     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 85: 'rule ifthenelse_split occ=0' 
635692     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 86: 'rule andLeft' 
635693     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 87: 'rule andLeft' 
635693     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 88: 'rule andLeft' 
635694     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 89: 'rule ifthenelse_split occ=0' 
635695     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 90: 'tryclose branch' 
635702     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 91: 'tryclose branch' 
635706     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 92: 'tryclose branch' 
635793     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 93: 'rule getOfSwap' 
635794     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 94: 'rule ifthenelse_negated' 
635795     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 95: 'rule ifthenelse_split occ=0' 
635796     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 96: 'rule andLeft' 
635797     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 97: 'rule andLeft' 
635797     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 98: 'rule andLeft' 
635798     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 99: 'rule ifthenelse_split occ=0' 
635799     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 100: 'tryclose branch' 
635865     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 101: 'tryclose branch' 
635870     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 102: 'tryclose branch' 
635963     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 103: 'cut '(int)s_0[v_x_0] = (int)s_0[v_y_0]'' 
635965     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 104: 'rule seqNPermInjective' 
635967     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 105: 'instantiate hide var=iv with='v_x_0'' 
635968     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 106: 'instantiate hide var=jv with='v_y_0'' 
635969     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 107: 'rule impLeft' 
635970     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 108: 'tryclose branch' 
636081     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 109: 'tryclose branch' 
636085     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 110: 'cut '(int)s_0[v_x_0] = v_x_0'' 
636086     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)'' 
636088     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 112: 'rule andRight' 
636089     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 113: 'rule andRight' 
636090     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 114: 'rule andRight' 
636090     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 115: 'rule andRight' 
636091     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 116: 'tryclose branch' 
636099     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 117: 'rule seqNPermSwapNPerm' 
636100     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 118: 'instantiate hide var=iv with='v_y_0'' 
636102     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 119: 'instantiate hide var=jv with='jv_1'' 
636102     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 120: 'tryclose branch' 
636186     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 121: 'rule allRight' 
636188     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 122: 'rule impRight' 
636189     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 123: 'rule andLeft' 
636190     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 124: 'instantiate var=iv with='v_iv_0'' 
636190     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 125: 'rule impLeft' 
636191     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 126: 'tryclose branch' 
636285     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 127: 'rule getOfSwap' 
636287     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 128: 'rule ifthenelse_negated' 
636288     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 129: 'rule ifthenelse_split occ=0' 
636289     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 130: 'rule andLeft' 
636290     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 131: 'rule andLeft' 
636290     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 132: 'rule andLeft' 
636291     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 133: 'rule ifthenelse_split occ=0' 
636292     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 134: 'tryclose branch' 
636368     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 135: 'rule ifthenelse_split occ=0' 
636370     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 136: 'tryclose branch' 
636440     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 137: 'instantiate var=iv with='v_y_0'' 
636441     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 138: 'rule impLeft' 
636441     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 139: 'tryclose branch' 
636445     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 140: 'tryclose branch' 
636449     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 141: 'tryclose branch' 
636453     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 142: 'tryclose branch' 
636614     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 143: 'rule getOfSwap' 
636615     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 144: 'rule ifthenelse_negated' 
636616     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 145: 'rule ifthenelse_split occ=0' 
636624     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 146: 'tryclose branch' 
636633     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 147: 'tryclose branch' 
636710     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 148: 'tryclose branch' 
640261     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 149: 'cut  '(int)s_0[v_y_0] = v_y_0'' 
640262     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)'' 
640268     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 151: 'rule andRight' 
640269     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 152: 'rule andRight' 
640270     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 153: 'rule andRight' 
640270     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 154: 'rule andRight' 
640271     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 155: 'tryclose branch' 
640280     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 156: 'rule seqNPermSwapNPerm' 
640281     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 157: 'instantiate hide var=iv with='v_x_0'' 
640282     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 158: 'instantiate hide var=jv with='jv_0'' 
640283     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 159: 'rule impLeft' 
640284     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 160: 'tryclose branch' 
640373     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 161: 'tryclose branch' 
640377     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 162: 'rule allRight' 
640379     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 163: 'rule impRight' 
640379     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 164: 'rule andLeft' 
640380     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 165: 'instantiate var=iv with='v_iv_0'' 
640381     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 166: 'rule impLeft' 
640382     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 167: 'tryclose branch' 
640474     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 168: 'rule getOfSwap' 
640476     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 169: 'rule ifthenelse_negated' 
640477     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 170: 'rule ifthenelse_split occ=0' 
640478     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 171: 'rule andLeft' 
640479     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 172: 'rule andLeft' 
640479     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 173: 'rule andLeft' 
640479     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 174: 'rule ifthenelse_split occ=0' 
640481     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 175: 'tryclose branch' 
640554     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 176: 'rule ifthenelse_split occ=0' 
640555     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 177: 'tryclose branch' 
640626     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 178: 'tryclose branch' 
640629     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 179: 'tryclose branch' 
640633     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 180: 'rule getOfSwap' 
640634     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 181: 'rule ifthenelse_negated' 
640635     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 182: 'rule ifthenelse_split occ=0' 
640636     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 183: 'tryclose branch' 
640645     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 184: 'tryclose branch' 
640721     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 185: 'rule getOfSwap' 
640722     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 186: 'rule ifthenelse_negated' 
640723     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 187: 'rule ifthenelse_split occ=0' 
640724     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 188: 'tryclose branch' 
640795     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 189: 'tryclose branch' 
640804     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 190: 'cut '(int)s_0[v_x_0]=v_y_0'' 
640805     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)'' 
640807     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 192: 'rule andRight' 
640807     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 193: 'rule andRight' 
640808     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 194: 'rule andRight' 
640809     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 195: 'rule andRight' 
640809     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 196: 'tryclose branch' 
640819     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 197: 'rule seqNPermSwapNPerm' 
640821     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 198: 'instantiate hide var=iv with='jv_0'' 
640822     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 199: 'instantiate hide var=jv with='v_x_0'' 
640822     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 200: 'rule impLeft' 
640823     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 201: 'tryclose branch' 
640907     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 202: 'rule seqNPermSwapNPerm formula='seqNPerm(seqSwap(s_0, jv_0, v_x_0))'' 
640909     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 203: 'instantiate hide var=iv with='jv_0'' 
640910     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 204: 'instantiate hide var=jv with='v_y_0'' 
640911     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 205: 'rule impLeft' 
640912     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 206: 'tryclose branch' 
640999     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 207: 'tryclose branch' 
641003     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 208: 'rule allRight' 
641004     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 209: 'rule impRight' 
641005     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 210: 'rule andLeft' 
641005     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 211: 'instantiate var=iv with='v_iv_0'' 
641006     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 212: 'rule impLeft' 
641006     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 213: 'tryclose branch' 
641101     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 214: 'rule getOfSwap' 
641103     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 215: 'rule ifthenelse_negated' 
641103     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 216: 'rule ifthenelse_split occ=0' 
641104     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 217: 'rule andLeft' 
641105     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 218: 'rule andLeft' 
641105     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 219: 'rule andLeft' 
641106     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 220: 'rule ifthenelse_split occ=0' 
641107     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 221: 'rule getOfSwap' 
641108     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 222: 'rule ifthenelse_negated' 
641108     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 223: 'rule ifthenelse_split occ=0' 
641109     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 224: 'rule andLeft' 
641110     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 225: 'rule andLeft' 
641110     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 226: 'rule andLeft' 
641110     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 227: 'rule ifthenelse_split occ=0' 
641111     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 228: 'tryclose branch' 
641199     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 229: 'rule ifthenelse_split occ=0' 
641200     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 230: 'tryclose branch' 
641206     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 231: 'tryclose branch' 
641281     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 232: 'tryclose branch' 
641359     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 233: 'rule ifthenelse_split' 
641360     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 234: 'rule getOfSwap' 
641361     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 235: 'rule ifthenelse_negated' 
641362     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 236: 'rule ifthenelse_split occ=0' 
641363     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 237: 'rule andLeft' 
641363     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 238: 'rule andLeft' 
641364     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 239: 'rule andLeft' 
641364     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 240: 'rule ifthenelse_split occ=0' 
641365     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 241: 'tryclose branch' 
641448     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 242: 'tryclose branch' 
641454     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 243: 'tryclose branch' 
641541     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 244: 'rule getOfSwap' 
641542     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 245: 'rule ifthenelse_negated' 
641543     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 246: 'rule ifthenelse_split occ=0' 
641544     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 247: 'rule andLeft' 
641544     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 248: 'rule andLeft' 
641544     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 249: 'rule andLeft' 
641545     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 250: 'rule ifthenelse_split occ=0' 
641545     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 251: 'tryclose branch' 
641550     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 252: 'rule ifthenelse_split occ=0' 
641551     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 253: 'tryclose branch' 
641628     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 254: 'tryclose branch' 
641674     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 255: 'tryclose branch' 
641679     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 256: 'tryclose branch' 
641774     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 257: 'rule getOfSwap' 
641775     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 258: 'rule ifthenelse_negated' 
641776     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 259: 'rule ifthenelse_split occ=0' 
641777     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 260: 'rule andLeft' 
641777     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 261: 'rule andLeft' 
641778     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 262: 'rule andLeft' 
641778     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 263: 'rule ifthenelse_split occ=0' 
641779     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 264: 'tryclose branch' 
641831     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 265: 'rule ifthenelse_split occ=0' 
641832     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 266: 'rule getOfSwap' 
641833     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 267: 'rule ifthenelse_negated' 
641833     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 268: 'rule ifthenelse_split occ=0' 
641834     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 269: 'tryclose branch' 
641839     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 270: 'tryclose branch' 
641844     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 271: 'tryclose branch' 
641956     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 272: 'tryclose branch' 
642041     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 273: 'rule getOfSwap' 
642042     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 274: 'rule ifthenelse_negated' 
642043     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 275: 'rule ifthenelse_split occ=0' 
642044     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 276: 'tryclose branch' 
642205     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 277: 'tryclose branch' 
642290     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 278: 'cut 'int::seqGet(s_0, v_y_0)=v_x_0'' 
642291     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 279: 'tryclose branch' 
645653     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 280: 'rule seqNPermSwapNPerm' 
645658     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 281: 'instantiate hide var=iv with='jv_1'' 
645659     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 282: 'instantiate hide var=jv with='v_y_0'' 
645660     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 283: 'rule impLeft' 
645661     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 284: 'tryclose branch' 
645773     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 285: 'rule seqNPermSwapNPerm formula='seqNPerm(seqSwap(s_0,jv_1,v_y_0))'' 
645774     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 286: 'instantiate hide var=iv with='jv_1'' 
645775     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 287: 'instantiate hide var=jv with='v_x_0'' 
645776     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 288: 'rule impLeft' 
645777     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 289: 'tryclose branch' 
645879     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 290: 'tryclose branch' 
648857     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 291: 'tryclose branch' 
651969     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 292: 'rule seqNPermSwapNPerm formula='seqNPerm(s_0)'' 
651974     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 293: 'instantiate hide var=iv with='v_x_0'' 
651975     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 294: 'instantiate hide var=jv with='jv_0'' 
651975     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 295: 'rule impLeft' 
651976     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 296: 'tryclose branch' 
652088     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 297: 'rule seqNPermSwapNPerm formula='seqNPerm(seqSwap(s_0,v_x_0,jv_0))'' 
652090     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 298: 'instantiate hide var=iv with='v_y_0'' 
652091     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 299: 'instantiate hide var=jv with='jv_1'' 
652092     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)' ...' 
652094     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 301: 'tryclose branch' 
653194     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm2/Taclet_schiffl_thm_1.proof 
653194     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 85.4ns 
653195     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
655598     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.4s 
655599     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: schiffl_thm_1 
656384     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: schiffl_thm_1 
656385     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 7.9ns 
656386     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 1: 'macro split-prop' 
656395     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 2: 'rule schiffl_lemma_2 formula='seqPerm(f_s, f_t)'' 
656406     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 3: 'instantiate hide var=x with='f_x'' 
656408     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 4: 'instantiate hide var=y with='f_y'' 
656410     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 5: 'rule impLeft' 
656411     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 6: 'tryclose branch' 
656415     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 7: 'rule exLeft' 
656417     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 8: 'macro split-prop' 
656420     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 9: 'rule seqPermDef occ=1' 
656423     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 10: 'rule andRight' 
656423     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 11: 'tryclose branch' 
656433     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 12: 'instantiate hide var=s with='r_0'' 
656435     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 13: 'rule andRight' 
656435     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 14: 'tryclose branch' 
656483     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 15: 'rule allRight' 
656484     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 16: 'rule impRight' 
656485     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 17: 'instantiate hide var=iv with='iv_0'' 
656485     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 18: 'rule impLeft' 
656486     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 19: 'tryclose branch' 
656545     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 20: 'rule andLeft' 
656545     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 21: 'rule seqNPermRange' 
656547     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 22: 'instantiate hide var=iv with='iv_0'' 
656547     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 23: 'rule impLeft' 
656548     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 24: 'tryclose branch' 
656551     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 25: 'rule andLeft' 
656551     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 26: 'rule andLeft' 
656551     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 27: 'rule seqNPermRange' 
656553     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 28: 'instantiate hide var=iv with='f_x'' 
656553     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 29: 'rule impLeft' 
656554     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 30: 'tryclose branch' 
656625     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 31: 'rule andLeft' 
656626     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 32: 'rule andLeft' 
656626     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 33: 'rule seqNPermRange' 
656627     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 34: 'instantiate hide var=iv with='f_y'' 
656628     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 35: 'rule impLeft' 
656629     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 36: 'tryclose branch' 
656707     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 37: 'rule andLeft' 
656707     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 38: 'rule andLeft' 
656708     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 39: 'rule getOfSeqDef occ=0' 
656709     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 40: 'rule getOfSeqDef' 
656709     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 41: 'rule ifthenelse_split occ=0' 
656710     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 42: 'rule andLeft occ=0' 
656711     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 43: 'rule sub_zero_2 occ=0' 
656711     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 44: 'rule ifthenelse_split occ=2' 
656712     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 45: 'rule andLeft' 
656712     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 46: 'rule sub_zero_2 occ=0' 
656713     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 47: 'rule add_zero_right occ=0' 
656713     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 48: 'rule add_zero_right occ=0' 
656714     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 49: 'rule add_zero_right occ=0' 
656714     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 50: 'rule add_zero_right occ=0' 
656715     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 51: 'rule add_zero_right occ=0' 
656715     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 52: 'rule add_zero_right occ=0' 
656716     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 53: 'rule ifthenelse_split occ=0' 
656717     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 54: 'rule ifthenelse_split occ=0' 
656717     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 55: 'tryclose branch' 
656720     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 56: 'tryclose branch' 
656755     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 57: 'rule ifthenelse_split occ=0' 
656756     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 58: 'tryclose branch' 
656813     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 59: 'rule ifthenelse_split occ=0' 
656814     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 60: 'rule seqNPermInjective' 
656816     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 61: 'instantiate hide var=iv with='iv_0'' 
656817     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 62: 'instantiate hide var=jv with='f_y'' 
656818     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 63: 'rule impLeft' 
656818     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 64: 'tryclose branch' 
656869     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 65: 'tryclose branch' 
656872     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 66: 'rule ifthenelse_split occ=0' 
656873     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 67: 'rule seqNPermInjective' 
656875     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 68: 'instantiate hide var=iv with='iv_0'' 
656876     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 69: 'instantiate hide var=jv with='f_x'' 
656877     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 70: 'rule impLeft' 
656877     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 71: 'tryclose branch' 
656930     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 72: 'tryclose branch' 
656933     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 73: 'tryclose branch' 
656936     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 74: 'tryclose branch' 
657001     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 75: 'tryclose branch' 
657064     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_eqSameSeq.proof 
657064     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 225ns 
657065     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
659490     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.42s 
659490     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: eqSameSeq 
660316     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: eqSameSeq 
660348     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 28.48ms