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

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

tests
0

failures
0

ignored
10m35.41s

duration
100%

successful

Tests

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

Standard output

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

1411       DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for Meta 
1413       DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for Meta 
1415       DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for Meta 
1415       DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for Meta 
2803       DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for JavaBigintExpression 
7896       DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 7.32s 
7965       INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof dummyTrue.key 
7996       DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 34.1ns 
8009       INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/firstOrder/Taclet_eqTermCut.proof 
8009       DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 186.71ns 
8013       INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
10686      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.67s 
10688      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: eqTermCut 
11660      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: eqTermCut 
11688      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 18.88ms 
11703      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/firstOrder/Taclet_equivAllRight.proof 
11703      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 181.81ns 
11705      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
14339      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.63s 
14340      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: equivAllRight 
15215      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: equivAllRight 
15227      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 9.46ms 
15230      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_irrflConcrete1.proof 
15231      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 510.62ns 
15232      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
17774      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.54s 
17775      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: irrflConcrete1 
18645      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: irrflConcrete1 
18651      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.58ms 
18655      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_irrflConcrete2.proof 
18655      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 365.22ns 
18656      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
21175      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.52s 
21175      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: irrflConcrete2 
21967      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: irrflConcrete2 
21978      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 7.05ms 
21981      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_cancel_gtPos.proof 
21982      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 571.72ns 
21983      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
24402      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.42s 
24402      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: cancel_gtPos 
25200      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: cancel_gtPos 
25236      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 32.79ms 
25237      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_cancel_gtNeg.proof 
25237      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 112.91ns 
25238      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
27621      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.38s 
27621      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: cancel_gtNeg 
28400      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: cancel_gtNeg 
28418      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 15.03ms 
28420      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intRulesIgnoringOF/Taclet_moduloIntIsInInt.proof 
28420      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 113.11ns 
28421      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
30836      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.42s 
30837      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: moduloIntIsInInt 
31622      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: moduloIntIsInInt 
31631      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 5.32ms 
31633      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intRulesIgnoringOF/Taclet_moduloLongIsInLong.proof 
31634      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 318.01ns 
31635      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
34006      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.37s 
34006      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: moduloLongIsInLong 
34813      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: moduloLongIsInLong 
34816      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 563.13ns 
34818      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intRulesIgnoringOF/Taclet_moduloShortIsInShort.proof 
34819      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 304.61ns 
34820      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
37182      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.36s 
37182      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: moduloShortIsInShort 
37955      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: moduloShortIsInShort 
37957      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 533.12ns 
37960      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intRulesIgnoringOF/Taclet_moduloByteIsInByte.proof 
37960      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 319.71ns 
37961      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
40335      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.37s 
40336      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: moduloByteIsInByte 
41117      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: moduloByteIsInByte 
41120      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 552.02ns 
41122      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intRulesIgnoringOF/Taclet_moduloCharIsInChar.proof 
41123      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 298.51ns 
41124      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
43535      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.41s 
43536      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: moduloCharIsInChar 
44308      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: moduloCharIsInChar 
44311      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 662.53ns 
44314      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_div_unique1.proof 
44314      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 333.21ns 
44315      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
46723      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.41s 
46724      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: div_unique1 
47496      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: div_unique1 
47535      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 34.77ms 
47538      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_div_unique2.proof 
47538      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 345.01ns 
47541      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
49975      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.43s 
49975      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: div_unique2 
50727      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: div_unique2 
50775      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 45.19ms 
50777      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_div_exists.proof 
50778      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 126.31ns 
50779      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
53146      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.37s 
53146      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: div_exists 
53932      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: div_exists 
54105      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 163.61ms 
54109      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_div_one.proof 
54110      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 508.62ns 
54111      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
56471      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.36s 
56472      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: div_one 
57244      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: div_one 
57249      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.25ms 
57251      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdiv_one.proof 
57251      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 318.91ns 
57252      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
59605      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.35s 
59606      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdiv_one 
60399      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdiv_one 
60402      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.09ms 
60405      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_div_zero.proof 
60405      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 326.01ns 
60410      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
62766      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.36s 
62767      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: div_zero 
63544      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: div_zero 
63586      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 36.8ms 
63590      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divResZero1.proof 
63590      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 226.91ns 
63591      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
65976      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.38s 
65976      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divResZero1 
66727      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divResZero1 
66738      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 8.13ms 
66740      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divResZero2.proof 
66740      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 102.2ns 
66741      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
69111      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.37s 
69111      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divResZero2 
69882      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divResZero2 
69892      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 7.78ms 
69894      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divResOne1.proof 
69894      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 119.3ns 
69895      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
72243      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.35s 
72244      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divResOne1 
73010      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divResOne1 
73021      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 8.38ms 
73024      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divResOne2.proof 
73024      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 316.61ns 
73025      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
75404      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.38s 
75405      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divResOne2 
76176      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divResOne2 
76187      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 8.06ms 
76189      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_div_cancel1.proof 
76189      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 307.51ns 
76190      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
78579      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.39s 
78580      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: div_cancel1 
79324      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: div_cancel1 
79343      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 15.77ms 
79345      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_div_cancel2.proof 
79345      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 119.7ns 
79346      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
81684      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.34s 
81685      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: div_cancel2 
82426      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: div_cancel2 
82429      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.17ms 
82430      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divAddMultDenom.proof 
82431      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 97.5ns 
82431      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
84776      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.34s 
84776      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divAddMultDenom 
85542      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divAddMultDenom 
85571      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 23.16ms 
85573      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divMinus.proof 
85573      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 286.71ns 
85574      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
87892      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.32s 
87892      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divMinus 
88655      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divMinus 
88696      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 35.06ms 
88697      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divMinusDenom.proof 
88698      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 91.8ns 
88698      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
91011      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.31s 
91011      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divMinusDenom 
91772      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divMinusDenom 
91801      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 23.25ms 
91803      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divLeastDPos.proof 
91803      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 168.01ns 
91804      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
94131      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.33s 
94131      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divLeastDPos 
94871      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divLeastDPos 
94877      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.02ms 
94879      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divLeastDNeg.proof 
94879      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 156ns 
94880      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
97203      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.32s 
97203      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divLeastDNeg 
97966      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divLeastDNeg 
97981      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 11.53ms 
97987      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divGreatestDPos.proof 
97987      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 110.4ns 
97988      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
100320     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.33s 
100321     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divGreatestDPos 
101083     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divGreatestDPos 
101096     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 11.27ms 
101100     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divGreatestDNeg.proof 
101101     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 307.51ns 
101104     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
103415     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.31s 
103415     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divGreatestDNeg 
104177     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divGreatestDNeg 
104184     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.9ms 
104185     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divIncreasingPos.proof 
104185     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 94.5ns 
104186     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
106508     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.32s 
106508     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divIncreasingPos 
107267     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divIncreasingPos 
107276     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 6.6ms 
107279     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divIncreasingNeg.proof 
107280     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 673.52ns 
107281     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
109611     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.33s 
109611     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divIncreasingNeg 
110350     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divIncreasingNeg 
110356     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.06ms 
110358     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdiv_zero.proof 
110358     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 84.6ns 
110358     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
112681     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.32s 
112681     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdiv_zero 
113441     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdiv_zero 
113445     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.48ms 
113446     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdivPulloutMinusNum.proof 
113446     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 84.4ns 
113447     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
115783     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.34s 
115784     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdivPulloutMinusNum 
116548     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdivPulloutMinusNum 
116557     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 6.73ms 
116558     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdivPulloutMinusDenom.proof 
116558     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 109.5ns 
116559     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
118911     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.35s 
118912     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdivPulloutMinusDenom 
119685     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdivPulloutMinusDenom 
119718     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 28ms 
119719     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdiv_uniquePosPos.proof 
119720     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 93.3ns 
119720     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
122093     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.37s 
122094     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdiv_uniquePosPos 
122837     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdiv_uniquePosPos 
122851     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 10.54ms 
122853     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdiv_uniquePosNeg.proof 
122853     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 310.81ns 
122854     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
125197     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.34s 
125197     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdiv_uniquePosNeg 
125943     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdiv_uniquePosNeg 
125993     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 47.91ms 
125995     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdiv_uniqueNegPos.proof 
125995     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 103.9ns 
125996     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
128322     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.33s 
128322     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdiv_uniqueNegPos 
129086     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdiv_uniqueNegPos 
129100     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 10.77ms 
129101     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdiv_uniqueNegNeg.proof 
129101     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 84.4ns 
129102     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
131454     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.35s 
131454     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdiv_uniqueNegNeg 
132217     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdiv_uniqueNegNeg 
132230     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 10.13ms 
132232     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdivMultDenom1.proof 
132232     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 98.8ns 
132232     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
134564     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.33s 
134564     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdivMultDenom1 
135327     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdivMultDenom1 
135357     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 25.16ms 
135358     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdivMultDenom2.proof 
135358     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 85.6ns 
135359     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
137706     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.35s 
137707     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdivMultDenom2 
138449     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdivMultDenom2 
138452     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 929.23ns 
138453     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_mod_geZero.proof 
138453     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 70.2ns 
138454     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
140784     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.33s 
140784     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: mod_geZero 
141541     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: mod_geZero 
141545     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.87ms 
141546     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_mod_lessDenom.proof 
141546     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 65.1ns 
141547     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
143853     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.31s 
143853     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: mod_lessDenom 
144615     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: mod_lessDenom 
144622     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.54ms 
144623     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmod_NumPos.proof 
144623     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 69.5ns 
144624     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
146919     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.3s 
146919     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmod_NumPos 
147674     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmod_NumPos 
147681     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.69ms 
147682     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmod_NumNeg.proof 
147682     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 65.1ns 
147683     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
149982     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.3s 
149983     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmod_NumNeg 
150739     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmod_NumNeg 
150754     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 11.47ms 
150755     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmod_geZero.proof 
150755     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 82.8ns 
150756     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
153070     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.31s 
153070     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmod_geZero 
153806     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmod_geZero 
153812     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.32ms 
153814     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmodNumZero.proof 
153814     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 66.8ns 
153814     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
156130     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.32s 
156131     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmodNumZero 
156915     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmodNumZero 
156918     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.62ms 
156921     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmod_pulloutminusNum.proof 
156921     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 248.3ns 
156922     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
159302     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.38s 
159303     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmod_pulloutminusNum 
160061     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmod_pulloutminusNum 
160065     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.22ms 
160066     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmod_pulloutminusDenom.proof 
160067     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 236.4ns 
160068     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
162370     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.3s 
162370     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmod_pulloutminusDenom 
163135     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmod_pulloutminusDenom 
163141     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.72ms 
163143     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmodUnique1.proof 
163143     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 84.8ns 
163144     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
165459     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.32s 
165460     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmodUnique1 
166197     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmodUnique1 
166246     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 40.61ms 
166248     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmodUnique2.proof 
166248     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 266.91ns 
166249     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
168570     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.32s 
168571     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmodUnique2 
169329     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmodUnique2 
169389     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 49.51ms 
169390     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_intDivRem.proof 
169390     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 79.6ns 
169391     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
171700     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.31s 
171701     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: intDivRem 
172455     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: intDivRem 
172458     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.33ms 
172459     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmodjmod.proof 
172459     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 70.1ns 
172460     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
174770     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.31s 
174770     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmodjmod 
175528     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmodjmod 
175554     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 23.04ms 
175556     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmodDivisible.proof 
175556     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 177.41ns 
175557     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
177903     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.35s 
177903     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmodDivisible 
178669     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmodDivisible 
178689     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 16.46ms 
178691     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmodDivisibleRep.proof 
178691     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 246.01ns 
178692     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
181050     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.36s 
181050     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmodDivisibleRep 
181792     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmodDivisibleRep 
181795     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 922.93ns 
181796     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdivAddMultDenom.proof 
181796     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 58.1ns 
181797     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
184138     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.34s 
184138     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdivAddMultDenom 
184897     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdivAddMultDenom 
184989     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 81.95ms 
184992     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmodAltZero.proof 
184992     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 226.11ns 
184993     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
187308     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.32s 
187309     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmodAltZero 
188073     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmodAltZero 
188082     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 6.03ms 
188083     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmodAddMultDenomZero.proof 
188084     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 240.71ns 
188085     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
190391     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.31s 
190391     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmodAddMultDenomZero 
191147     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmodAddMultDenomZero 
191153     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.92ms 
191154     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_polyDiv_zero.proof 
191154     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 70.6ns 
191155     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
193496     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.34s 
193496     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: polyDiv_zero 
194233     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: polyDiv_zero 
194246     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 10.17ms 
194247     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_polyMod_ltdivDenom.proof 
194247     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 86ns 
194248     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
196578     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.33s 
196578     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: polyMod_ltdivDenom 
197341     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: polyMod_ltdivDenom 
197351     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.31ms 
197353     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_empty.proof 
197353     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 62.4ns 
197354     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
199657     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.3s 
199657     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_empty 
200408     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_empty 
200411     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.34ms 
200413     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_induction_upper.proof 
200413     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 63ns 
200413     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
202714     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.3s 
202714     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_upper 
203470     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_induction_upper 
203473     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.57ms 
203474     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_induction_lower.proof 
203474     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 58.3ns 
203475     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
205786     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.31s 
205786     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_lower 
206543     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_induction_lower 
206556     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 10.27ms 
206558     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_bounds.proof 
206558     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 67.2ns 
206558     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
208880     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.32s 
208880     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_bounds 
209615     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_bounds 
209626     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 8.45ms 
209627     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_bounds2.proof 
209627     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 69ns 
209628     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
211951     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.32s 
211951     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_bounds2 
212704     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_bounds2 
212715     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 8.12ms 
212716     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_induction_upper2.proof 
212716     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 62.7ns 
212716     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
215012     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.3s 
215012     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_upper2 
215766     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_induction_upper2 
215769     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 859.22ns 
215770     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_induction_upper_concrete.proof 
215770     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 63.7ns 
215771     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
218074     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.3s 
218074     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_upper_concrete 
218827     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_induction_upper_concrete 
218830     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.61ms 
218831     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_induction_upper_concrete_2.proof 
218831     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 64.4ns 
218832     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
221124     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.29s 
221124     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_upper_concrete_2 
221878     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_induction_upper_concrete_2 
221883     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.63ms 
221885     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_induction_upper2_concrete.proof 
221885     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 209.31ns 
221886     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
224208     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.32s 
224208     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_upper2_concrete 
224942     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_induction_upper2_concrete 
224944     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 716.12ns 
224945     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_induction_lower_concrete.proof 
224945     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 55.6ns 
224946     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
227256     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.31s 
227256     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_lower_concrete 
228009     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_induction_lower_concrete 
228011     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 447.51ns 
228012     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_induction_lower2.proof 
228012     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 58.1ns 
228013     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
230312     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.3s 
230312     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_lower2 
231064     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_induction_lower2 
231067     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.4ms 
231068     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_induction_lower2_concrete.proof 
231068     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 54.5ns 
231069     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
233368     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.3s 
233369     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_lower2_concrete 
234130     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_induction_lower2_concrete 
234136     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.59ms 
234139     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_positive.proof 
234139     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 66.1ns 
234140     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
236480     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.34s 
236480     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_positive 
237221     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_positive 
237257     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 33.65ms 
237259     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_upper_bound.proof 
237259     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 212.6ns 
237260     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
239616     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.36s 
239616     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_upper_bound 
240364     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_upper_bound 
240389     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 21.27ms 
240390     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_lower_bound.proof 
240390     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 71.4ns 
240391     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
242740     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.35s 
242740     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_lower_bound 
243496     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_lower_bound 
243515     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 15.88ms 
243516     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_positive_lower_bound_element.proof 
243516     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 71.7ns 
243517     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
245838     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.32s 
245838     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_positive_lower_bound_element 
246594     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_positive_lower_bound_element 
246618     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 21.01ms 
246620     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_sub_same_index.proof 
246620     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 75.3ns 
246621     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
248940     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.32s 
248940     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_sub_same_index 
249708     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_sub_same_index 
249724     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 13.21ms 
249725     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_less_same_index.proof 
249725     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 59.2ns 
249726     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
252053     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.33s 
252054     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_less_same_index 
252793     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_less_same_index 
252826     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 27.96ms 
252827     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_equal_except_one_index.proof 
252827     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 73.4ns 
252828     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
255176     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.35s 
255176     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_equal_except_one_index 
255933     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_equal_except_one_index 
255949     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 12.95ms 
255950     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_is_max.proof 
255950     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 68.1ns 
255951     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
258266     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.31s 
258266     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_is_max 
259024     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_is_max 
259037     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 9.59ms 
259038     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_is_max2.proof 
259038     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 67.5ns 
259039     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
261337     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.3s 
261338     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_is_max2 
262095     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_is_max2 
262108     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 11.16ms 
262110     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_is_max3.proof 
262110     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 67.7ns 
262110     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
264411     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.3s 
264411     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_is_max3 
265166     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_is_max3 
265177     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 9.04ms 
265179     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_is_max4.proof 
265179     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 64.9ns 
265179     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
267493     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.31s 
267493     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_is_max4 
268226     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_is_max4 
268242     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 12.79ms 
268243     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_lt_max.proof 
268243     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 63.7ns 
268244     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
270559     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.32s 
270559     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_lt_max 
271315     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_lt_max 
271330     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 12.52ms 
271331     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_lt_max2.proof 
271331     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 70.2ns 
271332     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
273629     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.3s 
273630     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_lt_max2 
274384     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_lt_max2 
274400     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 12.6ms 
274401     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_lt_max3.proof 
274401     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 64.3ns 
274402     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
276718     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.32s 
276718     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_lt_max3 
277500     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_lt_max3 
277514     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 11.56ms 
277515     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_lt_max4.proof 
277515     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 72.4ns 
277516     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
279896     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.38s 
279896     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_lt_max4 
280632     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_lt_max4 
280646     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 10.49ms 
280647     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_gt0.proof 
280647     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 64.6ns 
280648     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
282963     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.32s 
282963     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_gt0 
283715     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_gt0 
283730     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 11.54ms 
283731     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_gt0_alt.proof 
283731     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 65.9ns 
283732     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
286026     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.29s 
286026     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_gt0_alt 
286778     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_gt0_alt 
286792     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 11.52ms 
286793     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_add_concrete.proof 
286794     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 64.4ns 
286794     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
289091     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.3s 
289091     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_add_concrete 
289845     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_add_concrete 
289850     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.33ms 
289851     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bprod/Taclet_bprod_all_positive.proof 
289851     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 47.2ns 
289852     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
292150     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.3s 
292150     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bprod_all_positive 
292915     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bprod_all_positive 
292926     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 8.03ms 
292927     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bprod/Taclet_bprod_split.proof 
292927     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 47.9ns 
292927     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
295263     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.34s 
295263     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bprod_split 
296003     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bprod_split 
296006     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.61ms 
296007     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powConcrete0.proof 
296007     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 57.4ns 
296008     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
298354     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.35s 
298354     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powConcrete0 
299114     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powConcrete0 
299119     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.39ms 
299121     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powConcrete1.proof 
299122     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 188.4ns 
299122     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
301455     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.33s 
301455     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powConcrete1 
302221     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powConcrete1 
302223     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 631.31ns 
302226     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powSplitFactor.proof 
302226     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 186.8ns 
302227     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
304633     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.41s 
304633     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powSplitFactor 
305419     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powSplitFactor 
305424     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.1ms 
305425     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powAdd.proof 
305425     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 52.3ns 
305426     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
307839     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.41s 
307839     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powAdd 
308600     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powAdd 
308605     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.18ms 
308606     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powMono.proof 
308606     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 53.7ns 
308607     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
310948     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.34s 
310948     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powMono 
311689     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powMono 
311698     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 7.31ms 
311699     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powMonoConcrete.proof 
311700     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 67ns 
311700     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
314032     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.33s 
314033     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powMonoConcrete 
314792     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powMonoConcrete 
314795     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.58ms 
314796     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powMonoConcreteRight.proof 
314796     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 48.5ns 
314797     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
317113     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.32s 
317113     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powMonoConcreteRight 
317873     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powMonoConcreteRight 
317875     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 425.21ns 
317876     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powPositive.proof 
317876     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 56.7ns 
317876     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
320177     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.3s 
320178     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powPositive 
320942     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powPositive 
320946     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.75ms 
320947     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powPositiveConcrete.proof 
320947     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 57.2ns 
320948     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
323264     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.32s 
323264     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powPositiveConcrete 
323998     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powPositiveConcrete 
324000     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 518.11ns 
324001     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powGeq1Concrete.proof 
324001     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 50.5ns 
324002     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
326312     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.31s 
326312     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powGeq1Concrete 
327067     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powGeq1Concrete 
327069     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 442.61ns 
327070     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_pow2InIntLower.proof 
327070     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 49.1ns 
327071     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
329365     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.29s 
329366     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: pow2InIntLower 
330120     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: pow2InIntLower 
330121     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 446.31ns 
330123     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_pow2InIntUpper.proof 
330123     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 58.1ns 
330123     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
332423     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.3s 
332423     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: pow2InIntUpper 
333176     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: pow2InIntUpper 
333179     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.52ms 
333181     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logSelfConcrete.proof 
333181     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 187.2ns 
333182     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
335470     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.29s 
335470     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logSelfConcrete 
336223     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logSelfConcrete 
336229     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.32ms 
336230     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_log1Concrete.proof 
336230     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 46.4ns 
336231     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
338537     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.31s 
338537     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: log1Concrete 
339273     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: log1Concrete 
339276     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.64ms 
339277     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logProduct.proof 
339277     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 54.4ns 
339278     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
341590     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.31s 
341590     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logProduct 
342343     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logProduct 
342348     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.1ms 
342349     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logTimesBaseConcrete.proof 
342349     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 46.9ns 
342349     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
344647     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.3s 
344647     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logTimesBaseConcrete 
345401     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logTimesBaseConcrete 
345404     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.83ms 
345405     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logProdIdentity.proof 
345405     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 47.6ns 
345406     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
347697     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.29s 
347698     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logProdIdentity 
348452     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logProdIdentity 
348463     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 8.49ms 
348465     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logProdIdentityConcrete.proof 
348465     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 179.4ns 
348466     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
350763     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.3s 
350763     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logProdIdentityConcrete 
351516     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logProdIdentityConcrete 
351519     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.49ms 
351520     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logPowIdentity.proof 
351520     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 48.1ns 
351521     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
353842     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.32s 
353842     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logPowIdentity 
354585     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logPowIdentity 
354588     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.01ms 
354589     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logPowIdentityConcrete.proof 
354589     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 56.1ns 
354590     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
356941     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.35s 
356941     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logPowIdentityConcrete 
357707     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logPowIdentityConcrete 
357711     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.59ms 
357712     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logPositive.proof 
357712     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 47.6ns 
357712     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
360044     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.33s 
360044     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logPositive 
360806     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logPositive 
360819     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 9.9ms 
360820     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logPositiveConcrete.proof 
360820     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 70ns 
360821     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
363137     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.32s 
363137     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logPositiveConcrete 
363898     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logPositiveConcrete 
363902     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 311.51ns 
363904     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logMono.proof 
363904     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 75.3ns 
363904     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
366236     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.33s 
366236     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logMono 
366977     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logMono 
367002     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 20.59ms 
367003     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logMonoConcrete.proof 
367003     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 61.6ns 
367004     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
369331     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.33s 
369331     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logMonoConcrete 
370091     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logMonoConcrete 
370094     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.34ms 
370095     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powLogLess.proof 
370095     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 48.9ns 
370096     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
372421     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.33s 
372421     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powLogLess 
373180     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powLogLess 
373194     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 11.49ms 
373195     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powLogMore2.proof 
373195     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 61.6ns 
373196     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
375508     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.31s 
375508     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powLogMore2 
376266     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powLogMore2 
376286     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 17.82ms 
376288     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logLessThanPow.proof 
376288     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 74.1ns 
376289     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
378627     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.34s 
378627     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logLessThanPow 
379364     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logLessThanPow 
379382     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 14.52ms 
379383     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logLessThanPowConcrete.proof 
379383     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 64.7ns 
379384     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
381700     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.32s 
381700     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logLessThanPowConcrete 
382458     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logLessThanPowConcrete 
382460     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 486.11ns 
382461     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logSqueeze.proof 
382461     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 49.2ns 
382462     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
384758     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.3s 
384758     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logSqueeze 
385512     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logSqueeze 
385517     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.88ms 
385518     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/booleanRules/Taclet_ifthenelse_equals.proof 
385518     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 51.8ns 
385518     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
387829     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.31s 
387829     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: ifthenelse_equals 
388566     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: ifthenelse_equals 
388569     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.22ms 
388571     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/booleanRules/Taclet_ifthenelse_equals_1.proof 
388571     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 169.2ns 
388572     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
390891     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.32s 
390891     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: ifthenelse_equals_1 
391648     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: ifthenelse_equals_1 
391650     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 691.91ns 
391651     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/booleanRules/Taclet_ifthenelse_equals_2.proof 
391652     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 49.9ns 
391652     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
393942     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.29s 
393942     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: ifthenelse_equals_2 
394699     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: ifthenelse_equals_2 
394701     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 613.01ns 
394702     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/locSet/Taclet_disjointWithSingleton1.proof 
394702     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 48.5ns 
394703     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
397011     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.31s 
397011     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: disjointWithSingleton1 
397750     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: disjointWithSingleton1 
397753     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 996.62ns 
397755     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/locSet/Taclet_disjointWithSingleton2.proof 
397755     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 48.6ns 
397755     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
400060     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.31s 
400060     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: disjointWithSingleton2 
400820     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: disjointWithSingleton2 
400822     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 947.91ns 
400823     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/locSet/Taclet_disjointArrayRanges.proof 
400823     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 57.6ns 
400824     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
403120     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.3s 
403120     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: disjointArrayRanges 
403879     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: disjointArrayRanges 
403886     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.7ms 
403887     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/locSet/Taclet_disjointArrayRangeAllFields1.proof 
403887     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 55.1ns 
403888     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
406203     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.32s 
406203     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: disjointArrayRangeAllFields1 
406942     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: disjointArrayRangeAllFields1 
406948     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.48ms 
406949     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/locSet/Taclet_disjointArrayRangeAllFields2.proof 
406949     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 50ns 
406950     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
409253     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.3s 
409253     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: disjointArrayRangeAllFields2 
410017     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: disjointArrayRangeAllFields2 
410023     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.17ms 
410025     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqSelfDefinition.proof 
410026     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 100ns 
410026     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
412324     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.3s 
412324     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqSelfDefinition 
413086     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqSelfDefinition 
413093     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 5.03ms 
413094     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqOutsideValue.proof 
413094     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 58.4ns 
413095     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
415420     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.33s 
415420     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqOutsideValue 
416187     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqOutsideValue 
416191     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.17ms 
416192     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_castedGetAny.proof 
416192     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 76ns 
416193     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
418513     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.32s 
418513     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: castedGetAny 
419283     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: castedGetAny 
419287     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.25ms 
419288     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqGetAlphaCast.proof 
419288     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 51ns 
419289     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
421635     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.35s 
421635     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqGetAlphaCast 
422383     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqGetAlphaCast 
422385     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 687.3ns 
422386     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqSingleton.proof 
422386     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 57.5ns 
422387     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
424714     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.33s 
424715     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqSingleton 
425486     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqSingleton 
425488     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 825.62ns 
425489     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqSingletonConcrete.proof 
425489     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 59.3ns 
425490     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
427805     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.32s 
427806     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqSingletonConcrete 
428572     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqSingletonConcrete 
428575     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 809.91ns 
428576     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqConcat.proof 
428577     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 166.4ns 
428577     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
430906     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.33s 
430906     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqConcat 
431674     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqConcat 
431682     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 5.86ms 
431683     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqSub.proof 
431683     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 62.5ns 
431684     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
434008     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.32s 
434008     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqSub 
434779     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqSub 
434782     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.07ms 
434783     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqReverse.proof 
434783     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 57.9ns 
434784     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
437108     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.32s 
437108     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqReverse 
437873     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqReverse 
437877     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.01ms 
437878     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqEmpty.proof 
437878     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 56.8ns 
437879     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
440184     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.3s 
440185     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqEmpty 
440949     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqEmpty 
440951     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 640.61ns 
440952     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqSingleton.proof 
440952     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 55.3ns 
440953     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
443267     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.31s 
443267     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqSingleton 
444027     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqSingleton 
444029     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 489.71ns 
444030     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqConcat.proof 
444030     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 56.5ns 
444031     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
446323     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.29s 
446323     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqConcat 
447086     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqConcat 
447091     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.13ms 
447093     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqSub.proof 
447093     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 78.6ns 
447093     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
449403     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.31s 
449403     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqSub 
450163     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqSub 
450165     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 680.61ns 
450166     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqReverse.proof 
450166     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 47ns 
450167     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
452463     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.3s 
452463     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqReverse 
453224     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqReverse 
453226     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 921.02ns 
453227     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_equalityToSeqGetAndSeqLenLeft.proof 
453227     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 49.4ns 
453228     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
455536     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.31s 
455536     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: equalityToSeqGetAndSeqLenLeft 
456298     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: equalityToSeqGetAndSeqLenLeft 
456300     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 975.32ns 
456301     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_equalityToSeqGetAndSeqLenRight.proof 
456301     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 64.3ns 
456302     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
458595     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.29s 
458595     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: equalityToSeqGetAndSeqLenRight 
459357     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: equalityToSeqGetAndSeqLenRight 
459360     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.86ms 
459361     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqSingletonEQ.proof 
459361     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 47.6ns 
459362     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
461675     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.31s 
461675     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqSingletonEQ 
462435     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqSingletonEQ 
462438     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 692.81ns 
462439     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqConcatEQ.proof 
462439     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 46.6ns 
462439     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
464749     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.31s 
464749     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqConcatEQ 
465491     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqConcatEQ 
465499     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 5.59ms 
465500     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqSubEQ.proof 
465500     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 48.6ns 
465500     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
467812     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.31s 
467812     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqSubEQ 
468572     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqSubEQ 
468573     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 436.81ns 
468575     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqReverseEQ.proof 
468575     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 56ns 
468575     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
470884     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.31s 
470884     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqReverseEQ 
471649     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqReverseEQ 
471654     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.17ms 
471655     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqEmptyEQ.proof 
471655     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 62.9ns 
471656     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
473955     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.3s 
473955     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqEmptyEQ 
474724     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqEmptyEQ 
474726     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 712.61ns 
474727     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqSingletonEQ.proof 
474727     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 53.1ns 
474728     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
477064     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.34s 
477064     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqSingletonEQ 
477834     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqSingletonEQ 
477836     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 594.61ns 
477837     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqConcatEQ.proof 
477837     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 70.1ns 
477838     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
480184     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.35s 
480184     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqConcatEQ 
480934     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqConcatEQ 
480937     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.69ms 
480939     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqSubEQ.proof 
480939     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 61.1ns 
480939     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
483288     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.35s 
483288     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqSubEQ 
484059     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqSubEQ 
484061     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 898.41ns 
484062     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqReverseEQ.proof 
484062     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 52.5ns 
484063     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
486393     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.33s 
486393     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqReverseEQ 
487159     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqReverseEQ 
487162     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.05ms 
487163     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqDefEQ.proof 
487163     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 56.6ns 
487164     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
489489     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.33s 
489489     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqDefEQ 
490237     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqDefEQ 
490240     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 971.82ns 
490241     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqDefEQ.proof 
490241     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 47.7ns 
490241     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
492564     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.32s 
492564     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqDefEQ 
493328     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqDefEQ 
493331     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.88ms 
493333     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqConcatWithSeqEmpty1.proof 
493333     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 54.4ns 
493333     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
495660     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.33s 
495660     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqConcatWithSeqEmpty1 
496425     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqConcatWithSeqEmpty1 
496432     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.82ms 
496433     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqConcatWithSeqEmpty2.proof 
496433     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 59.7ns 
496434     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
498759     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.33s 
498759     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqConcatWithSeqEmpty2 
499506     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqConcatWithSeqEmpty2 
499513     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 5.22ms 
499514     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqReverseOfSeqEmpty.proof 
499514     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 61.6ns 
499515     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
501829     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.31s 
501829     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqReverseOfSeqEmpty 
502591     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqReverseOfSeqEmpty 
502596     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.69ms 
502597     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_subSeqComplete.proof 
502597     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 51.1ns 
502598     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
504929     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.33s 
504929     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: subSeqComplete 
505694     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: subSeqComplete 
505700     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.79ms 
505701     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_subSeqTailR.proof 
505701     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 55.2ns 
505702     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
508028     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.33s 
508029     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: subSeqTailR 
508789     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: subSeqTailR 
508798     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 6.87ms 
508799     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_subSeqTailL.proof 
508799     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 56.7ns 
508799     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
511111     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.31s 
511112     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: subSeqTailL 
511853     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: subSeqTailL 
511862     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 6.99ms 
511863     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_subSeqTailEQR.proof 
511863     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 54.7ns 
511864     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
514170     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.31s 
514170     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: subSeqTailEQR 
514932     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: subSeqTailEQR 
514940     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 6.58ms 
514941     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_subSeqTailEQL.proof 
514941     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 47.2ns 
514942     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
517249     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.31s 
517249     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: subSeqTailEQL 
518012     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: subSeqTailEQL 
518019     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.53ms 
518020     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDef_split.proof 
518020     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 57.9ns 
518021     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
520340     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.32s 
520340     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_split 
521107     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDef_split 
521126     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 15.92ms 
521127     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDef_induction_upper.proof 
521127     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 52.9ns 
521128     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
523440     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.31s 
523440     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_induction_upper 
524204     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDef_induction_upper 
524224     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 17.48ms 
524225     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDef_induction_upper_concrete.proof 
524226     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 62.2ns 
524226     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
526519     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.29s 
526519     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_induction_upper_concrete 
527280     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDef_induction_upper_concrete 
527298     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 15.03ms 
527299     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDef_induction_lower.proof 
527299     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 55.4ns 
527299     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
529609     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.31s 
529609     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_induction_lower 
530369     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDef_induction_lower 
530386     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 14.16ms 
530387     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDef_induction_lower_concrete.proof 
530387     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 49.5ns 
530388     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
532694     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.31s 
532694     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_induction_lower_concrete 
533457     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDef_induction_lower_concrete 
533475     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 14.84ms 
533477     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDef_split_in_three.proof 
533477     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 52ns 
533477     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
535808     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.33s 
535808     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_split_in_three 
536573     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDef_split_in_three 
536618     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 38.59ms 
536620     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDef_empty.proof 
536620     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 64.3ns 
536621     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
538949     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.33s 
538949     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_empty 
539716     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDef_empty 
539721     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.53ms 
539722     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDef_one_summand.proof 
539722     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 49.3ns 
539722     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
542058     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.34s 
542058     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_one_summand 
542825     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDef_one_summand 
542829     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.82ms 
542830     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDef_lower_equals_upper.proof 
542830     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 60.9ns 
542831     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
545160     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.33s 
545160     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_lower_equals_upper 
545928     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDef_lower_equals_upper 
545931     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.78ms 
545932     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDefOfSeq.proof 
545932     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 48.6ns 
545933     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
548266     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.33s 
548266     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDefOfSeq 
549015     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDefOfSeq 
549053     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 35.6ms 
549055     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqSelfDefinitionEQ2.proof 
549055     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 63ns 
549055     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
551375     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.32s 
551375     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqSelfDefinitionEQ2 
552123     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqSelfDefinitionEQ2 
552129     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.84ms 
552130     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_indexOfSeqSingleton.proof 
552130     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 53.4ns 
552131     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
554463     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.33s 
554463     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: indexOfSeqSingleton 
555230     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: indexOfSeqSingleton 
555233     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.24ms 
555234     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_indexOfSeqConcatFirst.proof 
555235     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 61.5ns 
555235     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
557568     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.33s 
557568     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: indexOfSeqConcatFirst 
558334     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: indexOfSeqConcatFirst 
558343     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 6.99ms 
558344     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_indexOfSeqConcatSecond.proof 
558344     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 60.8ns 
558345     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
560658     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.31s 
560658     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: indexOfSeqConcatSecond 
561419     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: indexOfSeqConcatSecond 
561429     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 7.78ms 
561430     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_indexOfSeqSub.proof 
561430     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 57.9ns 
561431     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
563737     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.31s 
563738     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: indexOfSeqSub 
564499     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: indexOfSeqSub 
564511     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 9.62ms 
564512     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfArray2seq.proof 
564512     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 47.9ns 
564513     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
566818     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.31s 
566819     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfArray2seq 
567581     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfArray2seq 
567584     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 869.8ns 
567585     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getAnyOfArray2seq.proof 
567585     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 56ns 
567586     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
569892     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.31s 
569892     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getAnyOfArray2seq 
570656     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getAnyOfArray2seq 
570659     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.53ms 
570660     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfArray2seq.proof 
570660     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 49.2ns 
570660     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
572969     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.31s 
572969     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfArray2seq 
573733     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfArray2seq 
573738     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.59ms 
573739     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_getAnyOfNPermInv.proof 
573739     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 59.4ns 
573740     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
576045     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.31s 
576046     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getAnyOfNPermInv 
576808     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getAnyOfNPermInv 
576812     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.27ms 
576813     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqNPermRange.proof 
576813     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 52.8ns 
576814     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
579119     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.3s 
579119     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqNPermRange 
579881     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqNPermRange 
579920     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 33ms 
579921     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermTrans.proof 
579921     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 61ns 
579922     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
582245     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.32s 
582245     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermTrans 
583007     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermTrans 
583024     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 13.59ms 
583026     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermRefl.proof 
583026     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 200.6ns 
583027     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
585334     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.31s 
585334     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermRefl 
586096     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermRefl 
586107     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 8.15ms 
586108     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermSplit.proof 
586108     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 57.6ns 
586108     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
588428     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.32s 
588428     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermSplit 
589189     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermSplit 
589191     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 202.8ns 
589192     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqNPermRight.proof 
589192     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 46.6ns 
589193     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
591508     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.31s 
591508     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqNPermRight 
592272     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqNPermRight 
592347     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 64.25ms 
592348     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermFromSwap.proof 
592349     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 58ns 
592349     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
594673     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.32s 
594673     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermFromSwap 
595442     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermFromSwap 
595476     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 28.98ms 
595477     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermTransAlt0.proof 
595477     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 55.4ns 
595478     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
597807     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.33s 
597807     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermTransAlt0 
598578     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermTransAlt0 
598579     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 251.7ns 
598581     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermTransAlt1.proof 
598581     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 50.8ns 
598581     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
600915     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.33s 
600915     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermTransAlt1 
601687     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermTransAlt1 
601689     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 205.7ns 
601690     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermTransAlt2.proof 
601690     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 58ns 
601691     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
604016     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.33s 
604016     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermTransAlt2 
604783     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermTransAlt2 
604785     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 199ns 
604786     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermTransAlt3.proof 
604786     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 60.1ns 
604787     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
607118     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.33s 
607118     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermTransAlt3 
607886     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermTransAlt3 
607887     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 306.61ns 
607888     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermForall.proof 
607888     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 58.8ns 
607889     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
610269     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.38s 
610269     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermForall 
611044     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermForall 
611143     INFO  Test worker     d.u.i.k.s.SMTFocusResults Analyzing unsat core: (L_1 L_3 L_4) 
611151     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 103.61ms 
611154     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermExists.proof 
611154     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 199.2ns 
611158     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
613511     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.35s 
613512     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermExists 
614284     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermExists 
614324     INFO  Test worker     d.u.i.k.s.SMTFocusResults Analyzing unsat core: (L_1 L_3 L_5 L_6 L_7) 
614326     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 39.83ms 
614327     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm2/Taclet_schiffl_lemma_2.proof 
614327     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 70.1ns 
614328     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
616664     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.34s 
616664     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: schiffl_lemma_2 
617432     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: schiffl_lemma_2 
617434     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.5ns 
617457     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 1: 'macro split-prop' 
617490     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 2: 'rule allRight' 
617504     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 3: 'rule allRight' 
617507     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 4: 'macro split-prop' 
617516     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 5: 'rule 'seqPermDefLeft'' 
617517     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 6: 'rule 'andLeft'' 
617519     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 7: 'rule 'exLeft'' 
617520     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 8: 'macro split-prop' 
617523     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 9: 'rule  seqNPermRange' 
617524     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 10: 'instantiate var=iv with='v_x_0' occ=1' 
617526     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 11: 'rule impLeft' 
617528     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 12: 'tryclose branch' 
617739     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 13: 'rule andLeft' 
617740     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 14: 'rule andLeft' 
617741     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 15: 'instantiate var=iv with='v_y_0' occ=1' 
617743     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 16: 'rule impLeft' 
617745     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 17: 'tryclose branch' 
617900     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 18: 'rule andLeft' 
617901     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 19: 'rule andLeft' 
617904     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 20: 'rule seqNPermDefLeft' 
617906     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 21: 'instantiate var=iv with='v_x_0' occ=2' 
617908     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 22: 'rule impLeft' 
617910     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 23: 'tryclose branch' 
618097     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 24: 'rule exLeft' 
618099     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 25: 'rule andLeft' 
618100     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 26: 'rule andLeft' 
618101     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 27: 'instantiate hide var=iv with='v_y_0' occ=2' 
618103     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 28: 'rule impLeft' 
618106     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 29: 'tryclose branch' 
618254     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 30: 'rule exLeft' 
618255     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 31: 'rule andLeft' 
618255     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 32: 'rule andLeft' 
618258     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 33: 'instantiate var=iv with='jv_0' occ=1' 
618258     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 34: 'rule impLeft' 
618260     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 35: 'tryclose branch' 
618269     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 36: 'rule andLeft' 
618269     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 37: 'rule andLeft' 
618270     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 38: 'rule castAdd formula='s_0[jv_0] = v_x_0' occ=0' 
618272     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 39: 'instantiate hide var=iv with='jv_1' occ=1' 
618274     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 40: 'rule impLeft' 
618275     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 41: 'tryclose branch' 
618285     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 42: 'rule andLeft' 
618286     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 43: 'rule andLeft' 
618288     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 44: 'rule castAdd formula='s_0[jv_1] = v_y_0' occ=0' 
618288     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 45: 'instantiate var=iv  with='v_x_0'' 
618289     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 46: 'rule impLeft' 
618290     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 47: 'tryclose branch' 
618433     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 48: 'instantiate var=iv  with='v_y_0'' 
618434     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 49: 'rule impLeft' 
618435     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 50: 'tryclose branch' 
618558     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 51: 'cut 'v_x_0 = v_y_0'' 
618560     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)'' 
618562     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 53: 'rule andRight' 
618564     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 54: 'rule andRight' 
618565     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 55: 'rule andRight' 
618565     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 56: 'rule andRight' 
618567     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 57: 'rule lenOfSwap' 
618569     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 58: 'tryclose branch' 
618574     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 59: 'rule seqNPermSwapNPerm' 
618575     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 60: 'instantiate hide var='iv' with='v_x_0' occ=1' 
618577     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 61: 'instantiate hide var='jv' with='jv_0'' 
618578     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 62: 'rule impLeft' 
618579     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 63: 'tryclose branch' 
618686     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 64: 'tryclose branch' 
618691     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 65: 'rule allRight' 
618692     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 66: 'rule impRight' 
618693     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 67: 'rule andLeft' 
618694     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 68: 'instantiate var=iv with='v_iv_0'' 
618695     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 69: 'rule impLeft' 
618696     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 70: 'tryclose branch' 
618826     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 71: 'rule getOfSwap' 
618827     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 72: 'rule ifthenelse_negated' 
618828     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 73: 'rule ifthenelse_split occ=0' 
618830     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 74: 'rule andLeft' 
618831     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 75: 'rule andLeft' 
618832     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 76: 'rule andLeft' 
618833     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 77: 'rule ifthenelse_split occ=0' 
618834     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 78: 'tryclose branch' 
618939     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 79: 'rule ifthenelse_split occ=0' 
618941     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 80: 'tryclose branch' 
619081     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 81: 'tryclose branch' 
619085     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 82: 'tryclose branch' 
619091     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 83: 'rule getOfSwap' 
619092     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 84: 'rule ifthenelse_negated' 
619095     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 85: 'rule ifthenelse_split occ=0' 
619096     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 86: 'rule andLeft' 
619097     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 87: 'rule andLeft' 
619098     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 88: 'rule andLeft' 
619098     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 89: 'rule ifthenelse_split occ=0' 
619099     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 90: 'tryclose branch' 
619109     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 91: 'tryclose branch' 
619115     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 92: 'tryclose branch' 
619235     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 93: 'rule getOfSwap' 
619235     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 94: 'rule ifthenelse_negated' 
619237     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 95: 'rule ifthenelse_split occ=0' 
619238     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 96: 'rule andLeft' 
619239     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 97: 'rule andLeft' 
619240     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 98: 'rule andLeft' 
619242     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 99: 'rule ifthenelse_split occ=0' 
619243     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 100: 'tryclose branch' 
619296     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 101: 'tryclose branch' 
619303     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 102: 'tryclose branch' 
619400     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 103: 'cut '(int)s_0[v_x_0] = (int)s_0[v_y_0]'' 
619401     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 104: 'rule seqNPermInjective' 
619402     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 105: 'instantiate hide var=iv with='v_x_0'' 
619403     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 106: 'instantiate hide var=jv with='v_y_0'' 
619404     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 107: 'rule impLeft' 
619405     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 108: 'tryclose branch' 
619541     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 109: 'tryclose branch' 
619545     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 110: 'cut '(int)s_0[v_x_0] = v_x_0'' 
619547     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)'' 
619549     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 112: 'rule andRight' 
619551     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 113: 'rule andRight' 
619551     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 114: 'rule andRight' 
619552     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 115: 'rule andRight' 
619553     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 116: 'tryclose branch' 
619566     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 117: 'rule seqNPermSwapNPerm' 
619571     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 118: 'instantiate hide var=iv with='v_y_0'' 
619572     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 119: 'instantiate hide var=jv with='jv_1'' 
619574     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 120: 'tryclose branch' 
619677     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 121: 'rule allRight' 
619678     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 122: 'rule impRight' 
619679     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 123: 'rule andLeft' 
619680     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 124: 'instantiate var=iv with='v_iv_0'' 
619680     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 125: 'rule impLeft' 
619681     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 126: 'tryclose branch' 
619796     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 127: 'rule getOfSwap' 
619797     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 128: 'rule ifthenelse_negated' 
619798     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 129: 'rule ifthenelse_split occ=0' 
619799     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 130: 'rule andLeft' 
619800     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 131: 'rule andLeft' 
619800     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 132: 'rule andLeft' 
619801     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 133: 'rule ifthenelse_split occ=0' 
619802     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 134: 'tryclose branch' 
619895     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 135: 'rule ifthenelse_split occ=0' 
619897     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 136: 'tryclose branch' 
619983     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 137: 'instantiate var=iv with='v_y_0'' 
619984     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 138: 'rule impLeft' 
619985     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 139: 'tryclose branch' 
619990     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 140: 'tryclose branch' 
619995     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 141: 'tryclose branch' 
620000     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 142: 'tryclose branch' 
620145     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 143: 'rule getOfSwap' 
620146     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 144: 'rule ifthenelse_negated' 
620147     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 145: 'rule ifthenelse_split occ=0' 
620148     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 146: 'tryclose branch' 
620161     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 147: 'tryclose branch' 
620277     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 148: 'tryclose branch' 
624037     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 149: 'cut  '(int)s_0[v_y_0] = v_y_0'' 
624039     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)'' 
624048     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 151: 'rule andRight' 
624049     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 152: 'rule andRight' 
624050     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 153: 'rule andRight' 
624051     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 154: 'rule andRight' 
624051     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 155: 'tryclose branch' 
624060     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 156: 'rule seqNPermSwapNPerm' 
624060     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 157: 'instantiate hide var=iv with='v_x_0'' 
624061     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 158: 'instantiate hide var=jv with='jv_0'' 
624062     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 159: 'rule impLeft' 
624063     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 160: 'tryclose branch' 
624155     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 161: 'tryclose branch' 
624159     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 162: 'rule allRight' 
624159     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 163: 'rule impRight' 
624160     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 164: 'rule andLeft' 
624161     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 165: 'instantiate var=iv with='v_iv_0'' 
624161     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 166: 'rule impLeft' 
624162     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 167: 'tryclose branch' 
624258     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 168: 'rule getOfSwap' 
624260     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 169: 'rule ifthenelse_negated' 
624261     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 170: 'rule ifthenelse_split occ=0' 
624262     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 171: 'rule andLeft' 
624262     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 172: 'rule andLeft' 
624263     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 173: 'rule andLeft' 
624264     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 174: 'rule ifthenelse_split occ=0' 
624264     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 175: 'tryclose branch' 
624342     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 176: 'rule ifthenelse_split occ=0' 
624343     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 177: 'tryclose branch' 
624421     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 178: 'tryclose branch' 
624426     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 179: 'tryclose branch' 
624430     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 180: 'rule getOfSwap' 
624431     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 181: 'rule ifthenelse_negated' 
624432     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 182: 'rule ifthenelse_split occ=0' 
624432     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 183: 'tryclose branch' 
624443     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 184: 'tryclose branch' 
624527     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 185: 'rule getOfSwap' 
624528     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 186: 'rule ifthenelse_negated' 
624529     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 187: 'rule ifthenelse_split occ=0' 
624529     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 188: 'tryclose branch' 
624607     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 189: 'tryclose branch' 
624617     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 190: 'cut '(int)s_0[v_x_0]=v_y_0'' 
624617     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)'' 
624618     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 192: 'rule andRight' 
624620     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 193: 'rule andRight' 
624620     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 194: 'rule andRight' 
624621     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 195: 'rule andRight' 
624621     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 196: 'tryclose branch' 
624632     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 197: 'rule seqNPermSwapNPerm' 
624633     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 198: 'instantiate hide var=iv with='jv_0'' 
624634     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 199: 'instantiate hide var=jv with='v_x_0'' 
624635     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 200: 'rule impLeft' 
624636     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 201: 'tryclose branch' 
624723     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 202: 'rule seqNPermSwapNPerm formula='seqNPerm(seqSwap(s_0, jv_0, v_x_0))'' 
624724     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 203: 'instantiate hide var=iv with='jv_0'' 
624725     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 204: 'instantiate hide var=jv with='v_y_0'' 
624726     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 205: 'rule impLeft' 
624727     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 206: 'tryclose branch' 
624817     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 207: 'tryclose branch' 
624822     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 208: 'rule allRight' 
624823     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 209: 'rule impRight' 
624824     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 210: 'rule andLeft' 
624824     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 211: 'instantiate var=iv with='v_iv_0'' 
624825     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 212: 'rule impLeft' 
624825     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 213: 'tryclose branch' 
624923     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 214: 'rule getOfSwap' 
624924     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 215: 'rule ifthenelse_negated' 
624925     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 216: 'rule ifthenelse_split occ=0' 
624926     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 217: 'rule andLeft' 
624926     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 218: 'rule andLeft' 
624927     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 219: 'rule andLeft' 
624928     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 220: 'rule ifthenelse_split occ=0' 
624928     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 221: 'rule getOfSwap' 
624929     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 222: 'rule ifthenelse_negated' 
624930     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 223: 'rule ifthenelse_split occ=0' 
624931     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 224: 'rule andLeft' 
624931     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 225: 'rule andLeft' 
624932     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 226: 'rule andLeft' 
624932     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 227: 'rule ifthenelse_split occ=0' 
624933     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 228: 'tryclose branch' 
625020     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 229: 'rule ifthenelse_split occ=0' 
625021     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 230: 'tryclose branch' 
625027     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 231: 'tryclose branch' 
625105     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 232: 'tryclose branch' 
625186     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 233: 'rule ifthenelse_split' 
625187     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 234: 'rule getOfSwap' 
625188     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 235: 'rule ifthenelse_negated' 
625189     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 236: 'rule ifthenelse_split occ=0' 
625190     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 237: 'rule andLeft' 
625190     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 238: 'rule andLeft' 
625191     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 239: 'rule andLeft' 
625191     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 240: 'rule ifthenelse_split occ=0' 
625192     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 241: 'tryclose branch' 
625341     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 242: 'tryclose branch' 
625347     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 243: 'tryclose branch' 
625437     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 244: 'rule getOfSwap' 
625438     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 245: 'rule ifthenelse_negated' 
625439     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 246: 'rule ifthenelse_split occ=0' 
625440     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 247: 'rule andLeft' 
625440     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 248: 'rule andLeft' 
625441     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 249: 'rule andLeft' 
625441     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 250: 'rule ifthenelse_split occ=0' 
625442     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 251: 'tryclose branch' 
625447     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 252: 'rule ifthenelse_split occ=0' 
625448     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 253: 'tryclose branch' 
625526     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 254: 'tryclose branch' 
625531     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 255: 'tryclose branch' 
625536     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 256: 'tryclose branch' 
625634     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 257: 'rule getOfSwap' 
625635     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 258: 'rule ifthenelse_negated' 
625636     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 259: 'rule ifthenelse_split occ=0' 
625636     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 260: 'rule andLeft' 
625637     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 261: 'rule andLeft' 
625637     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 262: 'rule andLeft' 
625638     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 263: 'rule ifthenelse_split occ=0' 
625638     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 264: 'tryclose branch' 
625692     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 265: 'rule ifthenelse_split occ=0' 
625693     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 266: 'rule getOfSwap' 
625693     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 267: 'rule ifthenelse_negated' 
625694     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 268: 'rule ifthenelse_split occ=0' 
625694     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 269: 'tryclose branch' 
625700     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 270: 'tryclose branch' 
625705     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 271: 'tryclose branch' 
625818     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 272: 'tryclose branch' 
625904     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 273: 'rule getOfSwap' 
625905     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 274: 'rule ifthenelse_negated' 
625906     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 275: 'rule ifthenelse_split occ=0' 
625906     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 276: 'tryclose branch' 
626070     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 277: 'tryclose branch' 
626156     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 278: 'cut 'int::seqGet(s_0, v_y_0)=v_x_0'' 
626157     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 279: 'tryclose branch' 
629096     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 280: 'rule seqNPermSwapNPerm' 
629101     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 281: 'instantiate hide var=iv with='jv_1'' 
629102     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 282: 'instantiate hide var=jv with='v_y_0'' 
629102     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 283: 'rule impLeft' 
629103     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 284: 'tryclose branch' 
629215     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 285: 'rule seqNPermSwapNPerm formula='seqNPerm(seqSwap(s_0,jv_1,v_y_0))'' 
629216     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 286: 'instantiate hide var=iv with='jv_1'' 
629217     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 287: 'instantiate hide var=jv with='v_x_0'' 
629218     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 288: 'rule impLeft' 
629219     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 289: 'tryclose branch' 
629322     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 290: 'tryclose branch' 
632224     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 291: 'tryclose branch' 
635195     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 292: 'rule seqNPermSwapNPerm formula='seqNPerm(s_0)'' 
635199     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 293: 'instantiate hide var=iv with='v_x_0'' 
635200     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 294: 'instantiate hide var=jv with='jv_0'' 
635201     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 295: 'rule impLeft' 
635202     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 296: 'tryclose branch' 
635308     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 297: 'rule seqNPermSwapNPerm formula='seqNPerm(seqSwap(s_0,v_x_0,jv_0))'' 
635309     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 298: 'instantiate hide var=iv with='v_y_0'' 
635310     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 299: 'instantiate hide var=jv with='jv_1'' 
635311     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)' ...' 
635311     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 301: 'tryclose branch' 
636346     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm2/Taclet_schiffl_thm_1.proof 
636346     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 69.5ns 
636347     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
638759     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.41s 
638759     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: schiffl_thm_1 
639540     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: schiffl_thm_1 
639541     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 6.8ns 
639542     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 1: 'macro split-prop' 
639547     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 2: 'rule schiffl_lemma_2 formula='seqPerm(f_s, f_t)'' 
639556     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 3: 'instantiate hide var=x with='f_x'' 
639559     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 4: 'instantiate hide var=y with='f_y'' 
639561     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 5: 'rule impLeft' 
639562     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 6: 'tryclose branch' 
639566     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 7: 'rule exLeft' 
639566     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 8: 'macro split-prop' 
639570     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 9: 'rule seqPermDef occ=1' 
639570     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 10: 'rule andRight' 
639572     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 11: 'tryclose branch' 
639580     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 12: 'instantiate hide var=s with='r_0'' 
639580     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 13: 'rule andRight' 
639582     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 14: 'tryclose branch' 
639622     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 15: 'rule allRight' 
639623     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 16: 'rule impRight' 
639623     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 17: 'instantiate hide var=iv with='iv_0'' 
639624     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 18: 'rule impLeft' 
639624     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 19: 'tryclose branch' 
639688     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 20: 'rule andLeft' 
639688     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 21: 'rule seqNPermRange' 
639688     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 22: 'instantiate hide var=iv with='iv_0'' 
639689     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 23: 'rule impLeft' 
639690     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 24: 'tryclose branch' 
639693     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 25: 'rule andLeft' 
639694     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 26: 'rule andLeft' 
639694     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 27: 'rule seqNPermRange' 
639694     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 28: 'instantiate hide var=iv with='f_x'' 
639695     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 29: 'rule impLeft' 
639696     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 30: 'tryclose branch' 
639777     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 31: 'rule andLeft' 
639777     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 32: 'rule andLeft' 
639778     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 33: 'rule seqNPermRange' 
639778     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 34: 'instantiate hide var=iv with='f_y'' 
639779     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 35: 'rule impLeft' 
639780     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 36: 'tryclose branch' 
639869     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 37: 'rule andLeft' 
639869     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 38: 'rule andLeft' 
639870     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 39: 'rule getOfSeqDef occ=0' 
639871     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 40: 'rule getOfSeqDef' 
639871     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 41: 'rule ifthenelse_split occ=0' 
639872     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 42: 'rule andLeft occ=0' 
639872     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 43: 'rule sub_zero_2 occ=0' 
639873     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 44: 'rule ifthenelse_split occ=2' 
639874     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 45: 'rule andLeft' 
639874     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 46: 'rule sub_zero_2 occ=0' 
639875     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 47: 'rule add_zero_right occ=0' 
639875     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 48: 'rule add_zero_right occ=0' 
639875     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 49: 'rule add_zero_right occ=0' 
639876     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 50: 'rule add_zero_right occ=0' 
639876     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 51: 'rule add_zero_right occ=0' 
639877     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 52: 'rule add_zero_right occ=0' 
639877     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 53: 'rule ifthenelse_split occ=0' 
639878     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 54: 'rule ifthenelse_split occ=0' 
639878     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 55: 'tryclose branch' 
639881     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 56: 'tryclose branch' 
639921     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 57: 'rule ifthenelse_split occ=0' 
639922     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 58: 'tryclose branch' 
639980     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 59: 'rule ifthenelse_split occ=0' 
639981     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 60: 'rule seqNPermInjective' 
639982     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 61: 'instantiate hide var=iv with='iv_0'' 
639983     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 62: 'instantiate hide var=jv with='f_y'' 
639984     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 63: 'rule impLeft' 
639985     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 64: 'tryclose branch' 
640031     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 65: 'tryclose branch' 
640033     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 66: 'rule ifthenelse_split occ=0' 
640034     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 67: 'rule seqNPermInjective' 
640035     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 68: 'instantiate hide var=iv with='iv_0'' 
640036     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 69: 'instantiate hide var=jv with='f_x'' 
640037     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 70: 'rule impLeft' 
640037     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 71: 'tryclose branch' 
640085     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 72: 'tryclose branch' 
640088     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 73: 'tryclose branch' 
640091     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 74: 'tryclose branch' 
640139     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 75: 'tryclose branch' 
640189     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_eqSameSeq.proof 
640189     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 215.9ns 
640189     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
642608     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.42s 
642608     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: eqSameSeq 
643413     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: eqSameSeq 
643429     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 12.36ms