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

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

tests
0

failures
0

ignored
13m31.03s

duration
100%

successful

Tests

Test Method name Duration Result
powPositive data()[100] 4.114s passed
powPositiveConcrete data()[101] 3.900s passed
powGeq1Concrete data()[102] 3.930s passed
pow2InIntLower data()[103] 3.847s passed
pow2InIntUpper data()[104] 3.856s passed
logSelfConcrete data()[105] 3.884s passed
log1Concrete data()[106] 3.854s passed
logProduct data()[107] 3.902s passed
logTimesBaseConcrete data()[108] 4.171s passed
logProdIdentity data()[109] 3.948s passed
moduloByteIsInByte data()[10] 3.971s passed
logProdIdentityConcrete data()[110] 3.973s passed
logPowIdentity data()[111] 3.883s passed
logPowIdentityConcrete data()[112] 3.939s passed
logPositive data()[113] 3.931s passed
logPositiveConcrete data()[114] 3.886s passed
logMono data()[115] 3.938s passed
logMonoConcrete data()[116] 3.917s passed
powLogLess data()[117] 3.926s passed
powLogMore2 data()[118] 3.973s passed
logLessThanPow data()[119] 4.035s passed
moduloCharIsInChar data()[11] 3.955s passed
logLessThanPowConcrete data()[120] 3.920s passed
logSqueeze data()[121] 3.947s passed
ifthenelse_equals data()[122] 3.850s passed
ifthenelse_equals_1 data()[123] 3.924s passed
ifthenelse_equals_2 data()[124] 3.856s passed
disjointWithSingleton1 data()[125] 3.843s passed
disjointWithSingleton2 data()[126] 3.845s passed
disjointArrayRanges data()[127] 3.856s passed
disjointArrayRangeAllFields1 data()[128] 3.953s passed
disjointArrayRangeAllFields2 data()[129] 3.926s passed
div_unique1 data()[12] 4.019s passed
seqSelfDefinition data()[130] 3.910s passed
seqOutsideValue data()[131] 3.908s passed
castedGetAny data()[132] 3.850s passed
seqGetAlphaCast data()[133] 3.966s passed
getOfSeqSingleton data()[134] 3.885s passed
getOfSeqSingletonConcrete data()[135] 3.903s passed
getOfSeqConcat data()[136] 3.884s passed
getOfSeqSub data()[137] 3.981s passed
getOfSeqReverse data()[138] 3.902s passed
lenOfSeqEmpty data()[139] 3.925s passed
div_unique2 data()[13] 4.097s passed
lenOfSeqSingleton data()[140] 3.963s passed
lenOfSeqConcat data()[141] 3.952s passed
lenOfSeqSub data()[142] 3.985s passed
lenOfSeqReverse data()[143] 3.939s passed
equalityToSeqGetAndSeqLenLeft data()[144] 3.939s passed
equalityToSeqGetAndSeqLenRight data()[145] 3.956s passed
getOfSeqSingletonEQ data()[146] 4.004s passed
getOfSeqConcatEQ data()[147] 4.020s passed
getOfSeqSubEQ data()[148] 3.986s passed
getOfSeqReverseEQ data()[149] 3.931s passed
div_exists data()[14] 4.256s passed
lenOfSeqEmptyEQ data()[150] 3.923s passed
lenOfSeqSingletonEQ data()[151] 3.917s passed
lenOfSeqConcatEQ data()[152] 3.920s passed
lenOfSeqSubEQ data()[153] 3.913s passed
lenOfSeqReverseEQ data()[154] 3.946s passed
getOfSeqDefEQ data()[155] 3.915s passed
lenOfSeqDefEQ data()[156] 4.079s passed
seqConcatWithSeqEmpty1 data()[157] 4.018s passed
seqConcatWithSeqEmpty2 data()[158] 3.932s passed
seqReverseOfSeqEmpty data()[159] 3.956s passed
div_one data()[15] 4.027s passed
subSeqComplete data()[160] 3.940s passed
subSeqTailR data()[161] 3.965s passed
subSeqTailL data()[162] 3.952s passed
subSeqTailEQR data()[163] 3.977s passed
subSeqTailEQL data()[164] 3.970s passed
seqDef_split data()[165] 4.037s passed
seqDef_induction_upper data()[166] 4.107s passed
seqDef_induction_upper_concrete data()[167] 4.035s passed
seqDef_induction_lower data()[168] 4.015s passed
seqDef_induction_lower_concrete data()[169] 4.004s passed
jdiv_one data()[16] 4.049s passed
seqDef_split_in_three data()[170] 4.126s passed
seqDef_empty data()[171] 3.998s passed
seqDef_one_summand data()[172] 3.958s passed
seqDef_lower_equals_upper data()[173] 4.004s passed
seqDefOfSeq data()[174] 4.069s passed
seqSelfDefinitionEQ2 data()[175] 3.971s passed
indexOfSeqSingleton data()[176] 4.001s passed
indexOfSeqConcatFirst data()[177] 4.011s passed
indexOfSeqConcatSecond data()[178] 3.927s passed
indexOfSeqSub data()[179] 3.944s passed
div_zero data()[17] 4.056s passed
lenOfArray2seq data()[180] 3.940s passed
getAnyOfArray2seq data()[181] 3.939s passed
getOfArray2seq data()[182] 3.995s passed
getAnyOfNPermInv data()[183] 3.963s passed
seqNPermRange data()[184] 4.006s passed
seqPermTrans data()[185] 3.980s passed
seqPermRefl data()[186] 3.964s passed
seqPermSplit data()[187] 4.033s passed
seqNPermRight data()[188] 4.283s passed
seqPermFromSwap data()[189] 4.086s passed
divResZero1 data()[18] 3.993s passed
seqPermTransAlt0 data()[190] 3.963s passed
seqPermTransAlt1 data()[191] 4.118s passed
seqPermTransAlt2 data()[192] 3.997s passed
seqPermTransAlt3 data()[193] 3.952s passed
seqPermForall data()[194] 4.138s passed
seqPermExists data()[195] 4.111s passed
schiffl_lemma_2 data()[196] 27.493s passed
schiffl_thm_1 data()[197] 4.803s passed
eqSameSeq data()[198] 4.075s passed
divResZero2 data()[19] 4.066s passed
eqTermCut data()[1] 4.675s passed
divResOne1 data()[20] 4.057s passed
divResOne2 data()[21] 3.984s passed
div_cancel1 data()[22] 4.025s passed
div_cancel2 data()[23] 3.951s passed
divAddMultDenom data()[24] 3.991s passed
divMinus data()[25] 4.148s passed
divMinusDenom data()[26] 4.078s passed
divLeastDPos data()[27] 3.925s passed
divLeastDNeg data()[28] 4.028s passed
divGreatestDPos data()[29] 3.928s passed
equivAllRight data()[2] 4.368s passed
divGreatestDNeg data()[30] 4.025s passed
divIncreasingPos data()[31] 4.043s passed
divIncreasingNeg data()[32] 3.874s passed
jdiv_zero data()[33] 3.897s passed
jdivPulloutMinusNum data()[34] 4.068s passed
jdivPulloutMinusDenom data()[35] 4.140s passed
jdiv_uniquePosPos data()[36] 3.989s passed
jdiv_uniquePosNeg data()[37] 3.992s passed
jdiv_uniqueNegPos data()[38] 3.974s passed
jdiv_uniqueNegNeg data()[39] 4.229s passed
irrflConcrete1 data()[3] 4.246s passed
jdivMultDenom1 data()[40] 3.994s passed
jdivMultDenom2 data()[41] 4.000s passed
mod_geZero data()[42] 3.960s passed
mod_lessDenom data()[43] 3.939s passed
jmod_NumPos data()[44] 3.935s passed
jmod_NumNeg data()[45] 3.953s passed
jmod_geZero data()[46] 3.918s passed
jmodNumZero data()[47] 3.933s passed
jmod_pulloutminusNum data()[48] 3.939s passed
jmod_pulloutminusDenom data()[49] 3.886s passed
irrflConcrete2 data()[4] 4.219s passed
jmodUnique1 data()[50] 3.875s passed
jmodUnique2 data()[51] 3.927s passed
intDivRem data()[52] 3.785s passed
jmodjmod data()[53] 3.806s passed
jmodDivisible data()[54] 3.836s passed
jmodDivisibleRep data()[55] 3.777s passed
jdivAddMultDenom data()[56] 3.892s passed
jmodAltZero data()[57] 3.798s passed
jmodAddMultDenomZero data()[58] 4.018s passed
polyDiv_zero data()[59] 3.875s passed
cancel_gtPos data()[5] 4.223s passed
polyMod_ltdivDenom data()[60] 3.937s passed
bsum_empty data()[61] 3.880s passed
bsum_induction_upper data()[62] 3.839s passed
bsum_induction_lower data()[63] 3.867s passed
bsum_num_of_bounds data()[64] 3.811s passed
bsum_num_of_bounds2 data()[65] 3.747s passed
bsum_induction_upper2 data()[66] 3.752s passed
bsum_induction_upper_concrete data()[67] 3.794s passed
bsum_induction_upper_concrete_2 data()[68] 4.068s passed
bsum_induction_upper2_concrete data()[69] 3.969s passed
cancel_gtNeg data()[6] 4.059s passed
bsum_induction_lower_concrete data()[70] 3.886s passed
bsum_induction_lower2 data()[71] 3.901s passed
bsum_induction_lower2_concrete data()[72] 3.916s passed
bsum_positive data()[73] 4.044s passed
bsum_upper_bound data()[74] 3.898s passed
bsum_lower_bound data()[75] 3.945s passed
bsum_positive_lower_bound_element data()[76] 3.984s passed
bsum_sub_same_index data()[77] 4.019s passed
bsum_less_same_index data()[78] 4.010s passed
bsum_equal_except_one_index data()[79] 3.966s passed
moduloIntIsInInt data()[7] 4.197s passed
bsum_num_of_is_max data()[80] 3.899s passed
bsum_num_of_is_max2 data()[81] 3.952s passed
bsum_num_of_is_max3 data()[82] 3.898s passed
bsum_num_of_is_max4 data()[83] 3.980s passed
bsum_num_of_lt_max data()[84] 3.897s passed
bsum_num_of_lt_max2 data()[85] 4.009s passed
bsum_num_of_lt_max3 data()[86] 3.898s passed
bsum_num_of_lt_max4 data()[87] 3.938s passed
bsum_num_of_gt0 data()[88] 4.077s passed
bsum_num_of_gt0_alt data()[89] 3.958s passed
moduloLongIsInLong data()[8] 4.173s passed
bsum_add_concrete data()[90] 3.873s passed
bprod_all_positive data()[91] 3.907s passed
bprod_split data()[92] 3.872s passed
powConcrete0 data()[93] 3.910s passed
powConcrete1 data()[94] 3.980s passed
powSplitFactor data()[95] 3.895s passed
powAdd data()[96] 3.938s passed
powMono data()[97] 3.886s passed
powMonoConcrete data()[98] 4.130s passed
powMonoConcreteRight data()[99] 3.986s passed
moduloShortIsInShort data()[9] 3.990s passed

Standard output

410        INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src/test/resources/testcase/dummyTrue.key 
437        DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 12.49ms 
668        INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
688        WARN  Test worker     d.u.i.k.s.ProofSettings   No proof-settings could be loaded, using defaults java.io.FileNotFoundException: /home/runner/.key/proof-settings.props (No such file or directory)
	at java.base/java.io.FileInputStream.open0(Native Method)

1765       DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for Meta 
1767       DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for Meta 
1771       DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for Meta 
1771       DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for Meta 
3131       DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for JavaBigintExpression 
9815       DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 9.15s 
9881       INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof dummyTrue.key 
9920       DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 40.2ns 
9932       INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/firstOrder/Taclet_eqTermCut.proof 
9933       DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 216.72ns 
9937       INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
13352      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.42s 
13356      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: eqTermCut 
14561      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: eqTermCut 
14597      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 23.68ms 
14609      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/firstOrder/Taclet_equivAllRight.proof 
14610      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 166.91ns 
14611      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
17892      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.28s 
17893      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: equivAllRight 
18961      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: equivAllRight 
18976      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 11.94ms 
18978      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_irrflConcrete1.proof 
18979      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 159.41ns 
18980      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
22149      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.17s 
22149      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: irrflConcrete1 
23208      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: irrflConcrete1 
23222      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 10.23ms 
23224      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_irrflConcrete2.proof 
23224      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 163.91ns 
23225      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
26361      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.14s 
26361      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: irrflConcrete2 
27425      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: irrflConcrete2 
27440      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 10.67ms 
27443      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_cancel_gtPos.proof 
27443      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 154.91ns 
27444      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
30589      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.14s 
30589      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: cancel_gtPos 
31593      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: cancel_gtPos 
31662      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 64.96ms 
31667      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_cancel_gtNeg.proof 
31668      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 168.81ns 
31669      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
34686      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.02s 
34687      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: cancel_gtNeg 
35702      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: cancel_gtNeg 
35723      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 17.78ms 
35728      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intRulesIgnoringOF/Taclet_moduloIntIsInInt.proof 
35728      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 433.53ns 
35729      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
38866      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.14s 
38866      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: moduloIntIsInInt 
39918      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: moduloIntIsInInt 
39922      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 742.74ns 
39925      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intRulesIgnoringOF/Taclet_moduloLongIsInLong.proof 
39926      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 376.72ns 
39927      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
43066      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.14s 
43067      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: moduloLongIsInLong 
44092      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: moduloLongIsInLong 
44096      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 639.05ns 
44098      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intRulesIgnoringOF/Taclet_moduloShortIsInShort.proof 
44099      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 369.23ns 
44100      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
47089      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.99s 
47090      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: moduloShortIsInShort 
48083      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: moduloShortIsInShort 
48086      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 642.15ns 
48089      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intRulesIgnoringOF/Taclet_moduloByteIsInByte.proof 
48089      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 361.73ns 
48090      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
51048      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.96s 
51048      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: moduloByteIsInByte 
52053      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: moduloByteIsInByte 
52057      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 679.65ns 
52060      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intRulesIgnoringOF/Taclet_moduloCharIsInChar.proof 
52060      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 395.13ns 
52062      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
55023      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.96s 
55024      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: moduloCharIsInChar 
56009      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: moduloCharIsInChar 
56012      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 614.04ns 
56015      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_div_unique1.proof 
56015      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 441.53ns 
56017      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
58995      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.98s 
58996      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: div_unique1 
59981      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: div_unique1 
60031      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 46.59ms 
60045      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_div_unique2.proof 
60046      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 520.54ns 
60047      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
63054      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.01s 
63055      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: div_unique2 
64042      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: div_unique2 
64132      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 86.18ms 
64142      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_div_exists.proof 
64143      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 501.62ns 
64144      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
67144      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3s 
67145      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: div_exists 
68129      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: div_exists 
68394      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 255.17ms 
68397      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_div_one.proof 
68398      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 269.62ns 
68399      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
71397      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3s 
71398      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: div_one 
72416      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: div_one 
72422      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.6ms 
72424      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdiv_one.proof 
72424      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 134.61ns 
72425      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
75472      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.05s 
75473      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdiv_one 
76467      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdiv_one 
76471      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.48ms 
76475      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_div_zero.proof 
76476      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 324.42ns 
76477      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
79475      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3s 
79476      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: div_zero 
80484      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: div_zero 
80528      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 40.18ms 
80531      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divResZero1.proof 
80531      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 232.91ns 
80532      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
83494      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.96s 
83495      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divResZero1 
84503      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divResZero1 
84522      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 14.93ms 
84525      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divResZero2.proof 
84525      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 373.43ns 
84526      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
87580      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.05s 
87580      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divResZero2 
88572      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divResZero2 
88588      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 12.76ms 
88590      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divResOne1.proof 
88590      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 132.01ns 
88591      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
91604      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.01s 
91604      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divResOne1 
92627      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divResOne1 
92645      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 14.58ms 
92647      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divResOne2.proof 
92647      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 437.23ns 
92649      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
95622      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.97s 
95623      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divResOne2 
96609      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divResOne2 
96628      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 15.64ms 
96632      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_div_cancel1.proof 
96632      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 379.02ns 
96633      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
99607      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.97s 
99607      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: div_cancel1 
100626     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: div_cancel1 
100654     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 24.72ms 
100656     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_div_cancel2.proof 
100657     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 226.81ns 
100658     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
103619     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.96s 
103619     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: div_cancel2 
104602     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: div_cancel2 
104605     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.27ms 
104606     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divAddMultDenom.proof 
104606     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 111.21ns 
104608     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
107563     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.95s 
107563     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divAddMultDenom 
108549     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divAddMultDenom 
108596     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 41.34ms 
108598     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divMinus.proof 
108598     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 133.71ns 
108599     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
111655     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.06s 
111656     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divMinus 
112682     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divMinus 
112744     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 55.79ms 
112746     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divMinusDenom.proof 
112747     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 899.46ns 
112749     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
115778     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.03s 
115778     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divMinusDenom 
116773     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divMinusDenom 
116821     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 42.6ms 
116825     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divLeastDPos.proof 
116827     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 1.68ms 
116829     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
119763     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.93s 
119763     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divLeastDPos 
120737     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divLeastDPos 
120746     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 6.31ms 
120749     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divLeastDNeg.proof 
120750     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 361.82ns 
120751     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
123763     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.01s 
123763     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divLeastDNeg 
124761     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divLeastDNeg 
124775     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 11.76ms 
124777     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divGreatestDPos.proof 
124777     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 124.51ns 
124778     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
127721     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.94s 
127721     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divGreatestDPos 
128690     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divGreatestDPos 
128703     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 10.36ms 
128704     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divGreatestDNeg.proof 
128705     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 130.11ns 
128705     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
131654     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.95s 
131654     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divGreatestDNeg 
132716     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divGreatestDNeg 
132728     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 7.98ms 
132734     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divIncreasingPos.proof 
132735     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 134.51ns 
132736     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
135809     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.07s 
135834     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divIncreasingPos 
136767     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divIncreasingPos 
136775     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 5.53ms 
136776     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divIncreasingNeg.proof 
136777     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 114.71ns 
136777     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
139676     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.9s 
139677     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divIncreasingNeg 
140642     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divIncreasingNeg 
140649     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 5.33ms 
140651     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdiv_zero.proof 
140651     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 110.21ns 
140652     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
143577     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.92s 
143577     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdiv_zero 
144541     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdiv_zero 
144546     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.74ms 
144548     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdivPulloutMinusNum.proof 
144549     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 341.54ns 
144550     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
147594     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.04s 
147595     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdivPulloutMinusNum 
148601     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdivPulloutMinusNum 
148614     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 10.2ms 
148615     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdivPulloutMinusDenom.proof 
148616     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 125.91ns 
148617     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
151649     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.03s 
151650     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdivPulloutMinusDenom 
152690     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdivPulloutMinusDenom 
152754     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 58.58ms 
152764     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdiv_uniquePosPos.proof 
152764     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 475.44ns 
152772     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
155790     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.02s 
155790     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdiv_uniquePosPos 
156725     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdiv_uniquePosPos 
156744     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 15.95ms 
156746     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdiv_uniquePosNeg.proof 
156746     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 118.41ns 
156747     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
159737     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.99s 
159737     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdiv_uniquePosNeg 
160717     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdiv_uniquePosNeg 
160736     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 16.27ms 
160739     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdiv_uniqueNegPos.proof 
160739     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 287.02ns 
160740     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
163700     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.96s 
163701     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdiv_uniqueNegPos 
164667     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdiv_uniqueNegPos 
164709     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 38.73ms 
164712     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdiv_uniqueNegNeg.proof 
164712     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 371.03ns 
164714     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
167888     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.17s 
167888     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdiv_uniqueNegNeg 
168920     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdiv_uniqueNegNeg 
168939     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 15.22ms 
168941     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdivMultDenom1.proof 
168942     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 344.83ns 
168943     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
171897     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.95s 
171898     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdivMultDenom1 
172883     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdivMultDenom1 
172930     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 42.64ms 
172937     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdivMultDenom2.proof 
172937     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 127.01ns 
172938     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
175981     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.04s 
175981     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdivMultDenom2 
176929     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdivMultDenom2 
176935     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.25ms 
176937     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_mod_geZero.proof 
176937     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 84.81ns 
176939     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
179936     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3s 
179937     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: mod_geZero 
180884     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: mod_geZero 
180889     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.7ms 
180896     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_mod_lessDenom.proof 
180897     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 118.11ns 
180899     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
183876     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.98s 
183876     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: mod_lessDenom 
184825     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: mod_lessDenom 
184834     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 6.35ms 
184836     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmod_NumPos.proof 
184837     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 301.11ns 
184838     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
187809     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.97s 
187809     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmod_NumPos 
188759     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmod_NumPos 
188769     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 6.8ms 
188772     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmod_NumNeg.proof 
188772     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 321.43ns 
188773     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
191748     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.98s 
191748     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmod_NumNeg 
192703     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmod_NumNeg 
192723     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 16.57ms 
192724     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmod_geZero.proof 
192724     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 112.61ns 
192725     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
195686     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.96s 
195687     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmod_geZero 
196633     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmod_geZero 
196641     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 5.91ms 
196642     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmodNumZero.proof 
196642     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 113.71ns 
196643     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
199609     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.97s 
199609     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmodNumZero 
200567     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmodNumZero 
200571     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.39ms 
200577     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmod_pulloutminusNum.proof 
200577     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 359.21ns 
200578     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
203563     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.98s 
203564     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmod_pulloutminusNum 
204508     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmod_pulloutminusNum 
204512     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.04ms 
204516     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmod_pulloutminusDenom.proof 
204516     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 133.91ns 
204517     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
207473     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.96s 
207473     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmod_pulloutminusDenom 
208394     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmod_pulloutminusDenom 
208398     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.38ms 
208400     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmodUnique1.proof 
208400     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 97.21ns 
208401     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
211255     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.85s 
211256     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmodUnique1 
212176     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmodUnique1 
212272     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 87.88ms 
212278     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmodUnique2.proof 
212279     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 343.52ns 
212280     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
215214     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.93s 
215214     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmodUnique2 
216121     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmodUnique2 
216203     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 73.38ms 
216205     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_intDivRem.proof 
216205     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 115.11ns 
216206     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
219054     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.85s 
219054     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: intDivRem 
219984     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: intDivRem 
219988     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.64ms 
219990     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmodjmod.proof 
219990     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 170.11ns 
219991     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
222851     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.86s 
222851     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmodjmod 
223756     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmodjmod 
223794     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 34.11ms 
223796     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmodDivisible.proof 
223796     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 262.91ns 
223797     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
226682     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.89s 
226682     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmodDivisible 
227601     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmodDivisible 
227630     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 26.39ms 
227632     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmodDivisibleRep.proof 
227632     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 85.11ns 
227633     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
230476     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.84s 
230476     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmodDivisibleRep 
231404     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmodDivisibleRep 
231407     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.12ms 
231409     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdivAddMultDenom.proof 
231409     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 82.11ns 
231410     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
234237     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.83s 
234237     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdivAddMultDenom 
235150     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdivAddMultDenom 
235298     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 137.97ms 
235301     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmodAltZero.proof 
235301     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 295.02ns 
235303     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
238168     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.86s 
238168     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmodAltZero 
239085     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmodAltZero 
239097     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 9.73ms 
239098     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmodAddMultDenomZero.proof 
239099     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 100.01ns 
239099     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
242147     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.05s 
242147     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmodAddMultDenomZero 
243106     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmodAddMultDenomZero 
243115     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 6.91ms 
243116     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_polyDiv_zero.proof 
243117     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 91.01ns 
243117     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
246039     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.92s 
246039     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: polyDiv_zero 
246972     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: polyDiv_zero 
246990     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 15.28ms 
246992     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_polyMod_ltdivDenom.proof 
246992     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 85.61ns 
246993     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
249941     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.95s 
249941     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: polyMod_ltdivDenom 
250912     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: polyMod_ltdivDenom 
250926     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 7.53ms 
250929     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_empty.proof 
250929     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 99.81ns 
250930     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
253885     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.96s 
253886     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_empty 
254804     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_empty 
254807     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.71ms 
254809     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_induction_upper.proof 
254809     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 75.31ns 
254810     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
257718     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.91s 
257718     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_upper 
258641     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_induction_upper 
258646     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.16ms 
258648     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_induction_lower.proof 
258648     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 81.91ns 
258648     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
261551     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.9s 
261551     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_lower 
262486     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_induction_lower 
262513     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 24.12ms 
262515     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_bounds.proof 
262515     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 100.51ns 
262516     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
265403     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.89s 
265403     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_bounds 
266306     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_bounds 
266324     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 15.33ms 
266326     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_bounds2.proof 
266326     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 94.3ns 
266326     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
269141     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.81s 
269141     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_bounds2 
270052     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_bounds2 
270071     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 16.01ms 
270078     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_induction_upper2.proof 
270079     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 304.32ns 
270080     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
272913     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.83s 
272913     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_upper2 
273824     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_induction_upper2 
273829     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.93ms 
273831     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_induction_upper_concrete.proof 
273831     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 244.21ns 
273832     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
276679     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.85s 
276679     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_upper_concrete 
277617     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_induction_upper_concrete 
277622     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.91ms 
277624     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_induction_upper_concrete_2.proof 
277625     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 246.92ns 
277626     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
280631     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3s 
280631     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_upper_concrete_2 
281684     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_induction_upper_concrete_2 
281690     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.21ms 
281691     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_induction_upper2_concrete.proof 
281691     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 89.21ns 
281692     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
284719     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.03s 
284719     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_upper2_concrete 
285655     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_induction_upper2_concrete 
285659     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.58ms 
285660     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_induction_lower_concrete.proof 
285661     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 99.71ns 
285661     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
288602     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.94s 
288602     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_lower_concrete 
289543     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_induction_lower_concrete 
289546     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 748.25ns 
289547     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_induction_lower2.proof 
289547     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 72.81ns 
289548     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
292497     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.95s 
292497     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_lower2 
293442     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_induction_lower2 
293446     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.58ms 
293448     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_induction_lower2_concrete.proof 
293448     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 85.2ns 
293449     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
296403     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.95s 
296403     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_lower2_concrete 
297360     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_induction_lower2_concrete 
297362     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.08ms 
297364     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_positive.proof 
297364     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 75.81ns 
297365     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
300391     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.03s 
300391     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_positive 
301330     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_positive 
301406     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 73.33ms 
301409     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_upper_bound.proof 
301410     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 260.92ns 
301411     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
304333     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.92s 
304333     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_upper_bound 
305264     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_upper_bound 
305304     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 37.62ms 
305306     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_lower_bound.proof 
305306     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 89.41ns 
305307     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
308263     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.96s 
308264     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_lower_bound 
309209     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_lower_bound 
309249     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 36.19ms 
309250     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_positive_lower_bound_element.proof 
309250     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 90.31ns 
309251     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
312231     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.98s 
312231     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_positive_lower_bound_element 
313178     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_positive_lower_bound_element 
313233     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 51.2ms 
313235     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_sub_same_index.proof 
313235     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 125.11ns 
313236     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
316245     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.01s 
316245     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_sub_same_index 
317212     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_sub_same_index 
317252     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 36.9ms 
317255     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_less_same_index.proof 
317255     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 244.62ns 
317256     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
320254     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3s 
320254     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_less_same_index 
321201     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_less_same_index 
321262     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 56.16ms 
321265     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_equal_except_one_index.proof 
321265     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 259.12ns 
321266     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
324253     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.99s 
324253     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_equal_except_one_index 
325197     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_equal_except_one_index 
325229     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 27.69ms 
325230     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_is_max.proof 
325230     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 87.41ns 
325231     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
328168     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.94s 
328168     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_is_max 
329104     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_is_max 
329127     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 20.55ms 
329129     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_is_max2.proof 
329129     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 86ns 
329140     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
332108     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.97s 
332108     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_is_max2 
333047     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_is_max2 
333078     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 28.42ms 
333081     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_is_max3.proof 
333081     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 231.71ns 
333082     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
336028     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.95s 
336028     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_is_max3 
336954     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_is_max3 
336977     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 19.88ms 
336978     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_is_max4.proof 
336978     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 89ns 
336979     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
339975     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3s 
339975     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_is_max4 
340923     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_is_max4 
340957     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 30.41ms 
340958     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_lt_max.proof 
340958     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 91.81ns 
340959     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
343871     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.91s 
343871     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_lt_max 
344825     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_lt_max 
344854     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 26.28ms 
344856     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_lt_max2.proof 
344856     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 99.7ns 
344857     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
347813     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.96s 
347814     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_lt_max2 
348782     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_lt_max2 
348862     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 75.51ms 
348866     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_lt_max3.proof 
348866     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 266.52ns 
348870     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
351768     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.9s 
351768     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_lt_max3 
352734     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_lt_max3 
352762     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 25.49ms 
352764     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_lt_max4.proof 
352764     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 84.5ns 
352765     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
355681     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.92s 
355681     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_lt_max4 
356674     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_lt_max4 
356700     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 23.54ms 
356702     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_gt0.proof 
356702     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 75.4ns 
356703     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
359731     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.03s 
359731     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_gt0 
360746     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_gt0 
360777     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 27.87ms 
360779     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_gt0_alt.proof 
360779     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 87.11ns 
360780     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
363708     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.93s 
363708     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_gt0_alt 
364707     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_gt0_alt 
364735     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 25.62ms 
364737     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_add_concrete.proof 
364737     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 90.91ns 
364738     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
367635     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.9s 
367636     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_add_concrete 
368599     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_add_concrete 
368608     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 6.56ms 
368609     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bprod/Taclet_bprod_all_positive.proof 
368609     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 78.2ns 
368610     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
371523     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.91s 
371523     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bprod_all_positive 
372495     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bprod_all_positive 
372515     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 17.15ms 
372516     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bprod/Taclet_bprod_split.proof 
372516     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 70ns 
372517     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
375412     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.89s 
375412     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bprod_split 
376383     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bprod_split 
376388     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.45ms 
376389     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powConcrete0.proof 
376389     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 61.61ns 
376390     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
379311     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.92s 
379311     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powConcrete0 
380294     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powConcrete0 
380297     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 708.44ns 
380299     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powConcrete1.proof 
380299     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 59.2ns 
380299     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
383309     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.01s 
383310     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powConcrete1 
384275     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powConcrete1 
384277     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 843.97ns 
384279     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powSplitFactor.proof 
384279     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 63.2ns 
384280     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
387191     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.91s 
387191     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powSplitFactor 
388164     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powSplitFactor 
388172     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 5.68ms 
388174     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powAdd.proof 
388174     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 82.31ns 
388175     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
391136     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.96s 
391137     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powAdd 
392103     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powAdd 
392110     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.89ms 
392112     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powMono.proof 
392113     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 244.22ns 
392114     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
395004     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.89s 
395004     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powMono 
395983     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powMono 
395997     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 11.43ms 
395998     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powMonoConcrete.proof 
395998     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 80.41ns 
395999     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
399097     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.1s 
399098     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powMonoConcrete 
400120     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powMonoConcrete 
400126     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.38ms 
400128     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powMonoConcreteRight.proof 
400129     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 137.86ns 
400130     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
403093     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.96s 
403093     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powMonoConcreteRight 
404109     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powMonoConcreteRight 
404112     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 840.47ns 
404113     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powPositive.proof 
404113     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 106.51ns 
404114     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
407243     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.13s 
407243     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powPositive 
408219     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powPositive 
408226     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.34ms 
408227     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powPositiveConcrete.proof 
408227     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 82.22ns 
408228     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
411161     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.93s 
411161     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powPositiveConcrete 
412124     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powPositiveConcrete 
412126     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 804.18ns 
412128     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powGeq1Concrete.proof 
412128     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 62.41ns 
412129     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
415051     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.92s 
415051     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powGeq1Concrete 
416053     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powGeq1Concrete 
416056     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 784.98ns 
416057     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_pow2InIntLower.proof 
416057     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 61.01ns 
416058     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
418942     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.88s 
418942     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: pow2InIntLower 
419901     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: pow2InIntLower 
419903     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 669.37ns 
419904     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_pow2InIntUpper.proof 
419904     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 70.81ns 
419905     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
422788     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.88s 
422788     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: pow2InIntUpper 
423755     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: pow2InIntUpper 
423759     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.39ms 
423761     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logSelfConcrete.proof 
423761     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 80.61ns 
423761     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
426667     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.91s 
426667     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logSelfConcrete 
427633     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logSelfConcrete 
427644     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 8.13ms 
427645     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_log1Concrete.proof 
427645     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 66.71ns 
427646     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
430528     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.88s 
430528     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: log1Concrete 
431493     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: log1Concrete 
431497     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.69ms 
431499     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logProduct.proof 
431499     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 56.71ns 
431499     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
434403     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.9s 
434403     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logProduct 
435390     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logProduct 
435398     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 5.74ms 
435401     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logTimesBaseConcrete.proof 
435401     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 220.32ns 
435402     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
438584     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.18s 
438584     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logTimesBaseConcrete 
439565     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logTimesBaseConcrete 
439570     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.01ms 
439572     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logProdIdentity.proof 
439572     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 73.21ns 
439572     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
442515     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.94s 
442515     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logProdIdentity 
443488     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logProdIdentity 
443518     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 25.39ms 
443520     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logProdIdentityConcrete.proof 
443521     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 262.12ns 
443522     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
446522     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3s 
446522     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logProdIdentityConcrete 
447487     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logProdIdentityConcrete 
447491     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.13ms 
447493     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logPowIdentity.proof 
447493     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 73.3ns 
447494     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
450400     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.91s 
450400     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logPowIdentity 
451371     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logPowIdentity 
451374     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.41ms 
451376     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logPowIdentityConcrete.proof 
451376     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 59.91ns 
451376     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
454335     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.96s 
454335     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logPowIdentityConcrete 
455309     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logPowIdentityConcrete 
455314     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.45ms 
455315     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logPositive.proof 
455315     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 82.11ns 
455316     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
458249     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.93s 
458249     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logPositive 
459225     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logPositive 
459244     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 16.61ms 
459245     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logPositiveConcrete.proof 
459245     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 66.51ns 
459246     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
462155     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.91s 
462155     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logPositiveConcrete 
463124     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logPositiveConcrete 
463130     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 593.03ns 
463132     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logMono.proof 
463132     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 80.3ns 
463133     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
466048     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.92s 
466049     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logMono 
467023     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logMono 
467068     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 40.94ms 
467070     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logMonoConcrete.proof 
467070     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 81.61ns 
467071     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
470011     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.94s 
470011     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logMonoConcrete 
470982     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logMonoConcrete 
470986     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.85ms 
470987     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powLogLess.proof 
470987     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 58.91ns 
470988     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
473904     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.92s 
473905     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powLogLess 
474878     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powLogLess 
474911     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 30.84ms 
474924     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powLogMore2.proof 
474925     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 297.73ns 
474926     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
477867     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.94s 
477867     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powLogMore2 
478870     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powLogMore2 
478895     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 21.61ms 
478897     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logLessThanPow.proof 
478897     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 85.21ns 
478899     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
481929     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.03s 
481929     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logLessThanPow 
482902     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logLessThanPow 
482930     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 24.6ms 
482933     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logLessThanPowConcrete.proof 
482933     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 84.61ns 
482933     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
485879     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.95s 
485879     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logLessThanPowConcrete 
486849     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logLessThanPowConcrete 
486851     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 715.96ns 
486853     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logSqueeze.proof 
486853     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 57.81ns 
486854     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
489835     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.98s 
489835     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logSqueeze 
490793     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logSqueeze 
490799     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.28ms 
490800     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/booleanRules/Taclet_ifthenelse_equals.proof 
490800     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 64.21ns 
490801     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
493689     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.89s 
493690     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: ifthenelse_equals 
494644     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: ifthenelse_equals 
494648     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.91ms 
494651     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/booleanRules/Taclet_ifthenelse_equals_1.proof 
494651     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 225.22ns 
494652     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
497602     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.95s 
497602     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: ifthenelse_equals_1 
498570     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: ifthenelse_equals_1 
498573     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1ms 
498574     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/booleanRules/Taclet_ifthenelse_equals_2.proof 
498574     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 59.51ns 
498575     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
501456     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.88s 
501456     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: ifthenelse_equals_2 
502425     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: ifthenelse_equals_2 
502428     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1ms 
502431     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/locSet/Taclet_disjointWithSingleton1.proof 
502431     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 233.62ns 
502432     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
505306     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.87s 
505306     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: disjointWithSingleton1 
506269     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: disjointWithSingleton1 
506272     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.88ms 
506274     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/locSet/Taclet_disjointWithSingleton2.proof 
506274     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 69.9ns 
506275     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
509144     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.87s 
509145     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: disjointWithSingleton2 
510113     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: disjointWithSingleton2 
510117     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.81ms 
510118     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/locSet/Taclet_disjointArrayRanges.proof 
510118     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 80.41ns 
510119     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
512996     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.88s 
512997     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: disjointArrayRanges 
513963     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: disjointArrayRanges 
513974     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 8.39ms 
513975     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/locSet/Taclet_disjointArrayRangeAllFields1.proof 
513975     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 90.21ns 
513976     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
516876     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.9s 
516876     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: disjointArrayRangeAllFields1 
517909     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: disjointArrayRangeAllFields1 
517926     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 14.86ms 
517928     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/locSet/Taclet_disjointArrayRangeAllFields2.proof 
517929     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 98.01ns 
517929     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
520867     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.94s 
520867     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: disjointArrayRangeAllFields2 
521840     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: disjointArrayRangeAllFields2 
521853     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 11.13ms 
521855     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqSelfDefinition.proof 
521855     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 82.41ns 
521856     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
524734     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.88s 
524734     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqSelfDefinition 
525728     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqSelfDefinition 
525762     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 32.05ms 
525765     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqOutsideValue.proof 
525765     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 225.12ns 
525766     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
528689     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.92s 
528689     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqOutsideValue 
529666     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqOutsideValue 
529671     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.35ms 
529672     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_castedGetAny.proof 
529672     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 76.91ns 
529673     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
532547     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.87s 
532547     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: castedGetAny 
533515     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: castedGetAny 
533521     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 5ms 
533523     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqGetAlphaCast.proof 
533523     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 62.1ns 
533523     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
536476     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.95s 
536476     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqGetAlphaCast 
537485     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqGetAlphaCast 
537488     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 843.07ns 
537489     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqSingleton.proof 
537489     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 79.21ns 
537490     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
540391     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.9s 
540391     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqSingleton 
541369     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqSingleton 
541372     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.62ms 
541374     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqSingletonConcrete.proof 
541374     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 75.91ns 
541375     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
544292     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.92s 
544292     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqSingletonConcrete 
545273     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqSingletonConcrete 
545276     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.14ms 
545277     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqConcat.proof 
545277     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 68.7ns 
545278     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
548171     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.89s 
548171     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqConcat 
549146     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqConcat 
549159     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 10.83ms 
549160     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqSub.proof 
549160     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 82.31ns 
549161     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
552115     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.95s 
552115     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqSub 
553136     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqSub 
553141     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.87ms 
553142     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqReverse.proof 
553142     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 79.31ns 
553143     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
556077     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.93s 
556077     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqReverse 
557035     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqReverse 
557043     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 5.3ms 
557044     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqEmpty.proof 
557044     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 77.91ns 
557045     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
560004     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.96s 
560004     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqEmpty 
560965     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqEmpty 
560967     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 843.16ns 
560969     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqSingleton.proof 
560969     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 68.61ns 
560970     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
563925     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.96s 
563926     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqSingleton 
564928     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqSingleton 
564930     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 729.76ns 
564931     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqConcat.proof 
564931     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 74.61ns 
564932     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
567862     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.93s 
567862     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqConcat 
568878     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqConcat 
568882     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.37ms 
568883     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqSub.proof 
568884     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 78.11ns 
568884     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
571877     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.99s 
571877     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqSub 
572864     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqSub 
572867     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.53ms 
572869     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqReverse.proof 
572869     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 72.01ns 
572869     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
575815     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.95s 
575815     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqReverse 
576803     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqReverse 
576806     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.61ms 
576807     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_equalityToSeqGetAndSeqLenLeft.proof 
576808     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 62.6ns 
576808     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
579758     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.95s 
579758     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: equalityToSeqGetAndSeqLenLeft 
580742     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: equalityToSeqGetAndSeqLenLeft 
580745     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.42ms 
580747     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_equalityToSeqGetAndSeqLenRight.proof 
580747     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 73.31ns 
580747     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
583734     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.99s 
583734     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: equalityToSeqGetAndSeqLenRight 
584695     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: equalityToSeqGetAndSeqLenRight 
584701     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.15ms 
584703     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqSingletonEQ.proof 
584703     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 64.9ns 
584704     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
587681     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.98s 
587681     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqSingletonEQ 
588701     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqSingletonEQ 
588705     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.78ms 
588706     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqConcatEQ.proof 
588707     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 83.61ns 
588708     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
591721     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.01s 
591721     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqConcatEQ 
592712     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqConcatEQ 
592725     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 10.37ms 
592726     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqSubEQ.proof 
592726     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 82.51ns 
592727     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
595709     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.98s 
595709     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqSubEQ 
596708     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqSubEQ 
596711     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 804.56ns 
596713     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqReverseEQ.proof 
596713     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 73.91ns 
596714     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
599639     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.93s 
599639     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqReverseEQ 
600632     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqReverseEQ 
600643     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 7.61ms 
600644     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqEmptyEQ.proof 
600644     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 94.51ns 
600645     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
603565     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.92s 
603565     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqEmptyEQ 
604557     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqEmptyEQ 
604560     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.15ms 
604567     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqSingletonEQ.proof 
604568     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 339.12ns 
604569     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
607512     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.94s 
607512     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqSingletonEQ 
608480     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqSingletonEQ 
608482     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 837.65ns 
608484     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqConcatEQ.proof 
608484     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 68.9ns 
608484     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
611413     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.93s 
611413     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqConcatEQ 
612397     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqConcatEQ 
612402     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.6ms 
612403     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqSubEQ.proof 
612404     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 63.91ns 
612404     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
615324     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.92s 
615324     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqSubEQ 
616312     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqSubEQ 
616315     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.79ms 
616317     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqReverseEQ.proof 
616317     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 65.11ns 
616318     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
619263     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.95s 
619263     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqReverseEQ 
620257     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqReverseEQ 
620261     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.06ms 
620263     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqDefEQ.proof 
620263     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 255.42ns 
620264     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
623212     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.95s 
623212     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqDefEQ 
624172     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqDefEQ 
624176     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.42ms 
624177     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqDefEQ.proof 
624177     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 71.5ns 
624178     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
627259     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.08s 
627259     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqDefEQ 
628248     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqDefEQ 
628254     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.67ms 
628257     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqConcatWithSeqEmpty1.proof 
628257     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 179.31ns 
628258     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
631257     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3s 
631258     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqConcatWithSeqEmpty1 
632257     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqConcatWithSeqEmpty1 
632273     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 14.21ms 
632275     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqConcatWithSeqEmpty2.proof 
632275     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 76.41ns 
632276     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
635197     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.92s 
635197     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqConcatWithSeqEmpty2 
636187     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqConcatWithSeqEmpty2 
636205     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 15.42ms 
636206     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqReverseOfSeqEmpty.proof 
636206     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 75.81ns 
636207     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
639181     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.97s 
639182     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqReverseOfSeqEmpty 
640149     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqReverseOfSeqEmpty 
640161     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 9.98ms 
640163     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_subSeqComplete.proof 
640163     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 62.8ns 
640165     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
643107     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.94s 
643107     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: subSeqComplete 
644089     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: subSeqComplete 
644101     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 10.26ms 
644103     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_subSeqTailR.proof 
644103     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 67.2ns 
644103     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
647048     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.94s 
647048     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: subSeqTailR 
648037     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: subSeqTailR 
648067     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 27.37ms 
648068     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_subSeqTailL.proof 
648068     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 88.41ns 
648069     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
651025     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.96s 
651026     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: subSeqTailL 
651989     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: subSeqTailL 
652019     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 26.92ms 
652020     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_subSeqTailEQR.proof 
652020     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 83.41ns 
652021     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
654970     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.95s 
654971     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: subSeqTailEQR 
655968     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: subSeqTailEQR 
655996     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 24.93ms 
655997     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_subSeqTailEQL.proof 
655997     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 66.1ns 
655998     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
658946     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.95s 
658946     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: subSeqTailEQL 
659949     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: subSeqTailEQL 
659966     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 14.12ms 
659967     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDef_split.proof 
659967     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 91.7ns 
659968     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
663002     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.03s 
663002     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_split 
663967     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDef_split 
664002     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 30.83ms 
664003     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDef_induction_upper.proof 
664003     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 81.3ns 
664004     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
667000     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3s 
667000     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_induction_upper 
668046     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDef_induction_upper 
668109     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 59.9ms 
668111     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDef_induction_upper_concrete.proof 
668111     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 78.91ns 
668112     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
671101     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.99s 
671101     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_induction_upper_concrete 
672099     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDef_induction_upper_concrete 
672144     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 41.88ms 
672146     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDef_induction_lower.proof 
672146     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 80.81ns 
672147     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
675113     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.97s 
675113     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_induction_lower 
676110     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDef_induction_lower 
676159     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 45.4ms 
676160     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDef_induction_lower_concrete.proof 
676160     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 84.7ns 
676161     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
679114     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.95s 
679114     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_induction_lower_concrete 
680111     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDef_induction_lower_concrete 
680163     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 48.3ms 
680165     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDef_split_in_three.proof 
680165     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 65.8ns 
680166     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
683173     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.01s 
683173     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_split_in_three 
684136     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDef_split_in_three 
684289     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 142.99ms 
684290     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDef_empty.proof 
684291     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 64.5ns 
684291     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
687276     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.98s 
687276     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_empty 
688279     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDef_empty 
688287     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 6.71ms 
688289     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDef_one_summand.proof 
688289     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 63.4ns 
688290     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
691246     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.96s 
691246     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_one_summand 
692237     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDef_one_summand 
692245     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 6.7ms 
692247     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDef_lower_equals_upper.proof 
692247     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 74.3ns 
692248     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
695251     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3s 
695251     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_lower_equals_upper 
696243     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDef_lower_equals_upper 
696249     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.18ms 
696250     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDefOfSeq.proof 
696251     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 79.31ns 
696251     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
699297     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.05s 
699297     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDefOfSeq 
700297     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDefOfSeq 
700318     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 17.79ms 
700320     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqSelfDefinitionEQ2.proof 
700320     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 85.5ns 
700321     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
703295     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.97s 
703295     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqSelfDefinitionEQ2 
704277     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqSelfDefinitionEQ2 
704289     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 10.24ms 
704291     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_indexOfSeqSingleton.proof 
704291     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 83.8ns 
704292     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
707256     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.96s 
707256     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: indexOfSeqSingleton 
708285     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: indexOfSeqSingleton 
708291     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.85ms 
708292     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_indexOfSeqConcatFirst.proof 
708292     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 80ns 
708293     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
711258     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.96s 
711258     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: indexOfSeqConcatFirst 
712249     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: indexOfSeqConcatFirst 
712302     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 49.86ms 
712303     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_indexOfSeqConcatSecond.proof 
712303     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 98.31ns 
712304     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
715221     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.92s 
715221     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: indexOfSeqConcatSecond 
716209     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: indexOfSeqConcatSecond 
716228     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 16.2ms 
716230     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_indexOfSeqSub.proof 
716230     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 74.8ns 
716230     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
719173     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.94s 
719173     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: indexOfSeqSub 
720148     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: indexOfSeqSub 
720172     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 21.88ms 
720174     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfArray2seq.proof 
720174     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 79.31ns 
720175     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
723121     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.95s 
723121     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfArray2seq 
724109     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfArray2seq 
724112     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.45ms 
724114     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getAnyOfArray2seq.proof 
724114     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 74.81ns 
724114     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
727080     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.97s 
727080     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getAnyOfArray2seq 
728047     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getAnyOfArray2seq 
728052     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.39ms 
728053     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfArray2seq.proof 
728053     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 59.9ns 
728054     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
730992     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.94s 
730992     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfArray2seq 
732038     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfArray2seq 
732046     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 5.9ms 
732048     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_getAnyOfNPermInv.proof 
732048     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 135.61ns 
732049     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
735015     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.97s 
735016     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getAnyOfNPermInv 
736002     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getAnyOfNPermInv 
736010     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 5.23ms 
736011     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqNPermRange.proof 
736011     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 59.7ns 
736012     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
738943     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.93s 
738943     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqNPermRange 
739933     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqNPermRange 
740015     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 75.98ms 
740017     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermTrans.proof 
740017     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 87.81ns 
740018     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
742974     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.96s 
742974     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermTrans 
743964     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermTrans 
743995     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 27.52ms 
743996     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermRefl.proof 
743996     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 76.5ns 
743997     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
746946     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.95s 
746946     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermRefl 
747934     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermRefl 
747959     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 22.55ms 
747961     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermSplit.proof 
747961     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 81.5ns 
747961     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
750996     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.03s 
750996     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermSplit 
751990     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermSplit 
751992     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 324.82ns 
751994     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqNPermRight.proof 
751994     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 60.2ns 
751995     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
755022     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.03s 
755022     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqNPermRight 
755995     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqNPermRight 
756274     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 268.09ms 
756276     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermFromSwap.proof 
756276     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 79.9ns 
756277     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
759264     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.99s 
759264     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermFromSwap 
760303     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermFromSwap 
760361     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 53.1ms 
760362     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermTransAlt0.proof 
760362     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 64.3ns 
760363     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
763328     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.97s 
763328     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermTransAlt0 
764322     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermTransAlt0 
764324     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 384.02ns 
764326     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermTransAlt1.proof 
764326     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 62.6ns 
764326     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
767408     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.08s 
767409     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermTransAlt1 
768440     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermTransAlt1 
768443     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 412.12ns 
768444     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermTransAlt2.proof 
768444     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 81.4ns 
768445     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
771444     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3s 
771444     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermTransAlt2 
772437     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermTransAlt2 
772439     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 451.33ns 
772441     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermTransAlt3.proof 
772441     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 60.1ns 
772442     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
775395     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.95s 
775395     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermTransAlt3 
776389     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermTransAlt3 
776391     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 614.13ns 
776393     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermForall.proof 
776393     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 75.8ns 
776394     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
779394     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3s 
779394     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermForall 
780387     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermForall 
780509     INFO  Test worker     d.u.i.k.s.SMTFocusResults Analyzing unsat core: (L_1 L_3 L_4) 
780529     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 139.11ms 
780532     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermExists.proof 
780532     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 246.01ns 
780534     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
783595     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.06s 
783595     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermExists 
784585     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermExists 
784641     INFO  Test worker     d.u.i.k.s.SMTFocusResults Analyzing unsat core: (L_1 L_3 L_5 L_6 L_7) 
784642     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 54.63ms 
784643     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm2/Taclet_schiffl_lemma_2.proof 
784643     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 67.6ns 
784644     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
787691     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.05s 
787691     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: schiffl_lemma_2 
788688     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: schiffl_lemma_2 
788690     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.1ns 
788720     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 1: 'macro split-prop' 
788787     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 2: 'rule allRight' 
788811     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 3: 'rule allRight' 
788825     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 4: 'macro split-prop' 
788835     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 5: 'rule 'seqPermDefLeft'' 
788838     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 6: 'rule 'andLeft'' 
788839     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 7: 'rule 'exLeft'' 
788842     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 8: 'macro split-prop' 
788844     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 9: 'rule  seqNPermRange' 
788846     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 10: 'instantiate var=iv with='v_x_0' occ=1' 
788849     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 11: 'rule impLeft' 
788850     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 12: 'tryclose branch' 
789026     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 13: 'rule andLeft' 
789027     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 14: 'rule andLeft' 
789028     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 15: 'instantiate var=iv with='v_y_0' occ=1' 
789029     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 16: 'rule impLeft' 
789031     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 17: 'tryclose branch' 
789156     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 18: 'rule andLeft' 
789157     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 19: 'rule andLeft' 
789161     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 20: 'rule seqNPermDefLeft' 
789163     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 21: 'instantiate var=iv with='v_x_0' occ=2' 
789164     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 22: 'rule impLeft' 
789167     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 23: 'tryclose branch' 
789371     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 24: 'rule exLeft' 
789374     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 25: 'rule andLeft' 
789375     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 26: 'rule andLeft' 
789376     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 27: 'instantiate hide var=iv with='v_y_0' occ=2' 
789378     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 28: 'rule impLeft' 
789381     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 29: 'tryclose branch' 
789534     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 30: 'rule exLeft' 
789536     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 31: 'rule andLeft' 
789538     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 32: 'rule andLeft' 
789539     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 33: 'instantiate var=iv with='jv_0' occ=1' 
789540     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 34: 'rule impLeft' 
789542     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 35: 'tryclose branch' 
789551     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 36: 'rule andLeft' 
789557     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 37: 'rule andLeft' 
789559     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 38: 'rule castAdd formula='s_0[jv_0] = v_x_0' occ=0' 
789562     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 39: 'instantiate hide var=iv with='jv_1' occ=1' 
789565     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 40: 'rule impLeft' 
789566     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 41: 'tryclose branch' 
789578     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 42: 'rule andLeft' 
789580     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 43: 'rule andLeft' 
789581     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 44: 'rule castAdd formula='s_0[jv_1] = v_y_0' occ=0' 
789582     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 45: 'instantiate var=iv  with='v_x_0'' 
789583     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 46: 'rule impLeft' 
789584     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 47: 'tryclose branch' 
789779     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 48: 'instantiate var=iv  with='v_y_0'' 
789780     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 49: 'rule impLeft' 
789781     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 50: 'tryclose branch' 
789959     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 51: 'cut 'v_x_0 = v_y_0'' 
789964     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)'' 
789967     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 53: 'rule andRight' 
789968     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 54: 'rule andRight' 
789969     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 55: 'rule andRight' 
789971     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 56: 'rule andRight' 
789972     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 57: 'rule lenOfSwap' 
789975     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 58: 'tryclose branch' 
789982     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 59: 'rule seqNPermSwapNPerm' 
789984     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 60: 'instantiate hide var='iv' with='v_x_0' occ=1' 
789986     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 61: 'instantiate hide var='jv' with='jv_0'' 
789987     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 62: 'rule impLeft' 
789988     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 63: 'tryclose branch' 
790115     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 64: 'tryclose branch' 
790119     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 65: 'rule allRight' 
790121     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 66: 'rule impRight' 
790122     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 67: 'rule andLeft' 
790123     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 68: 'instantiate var=iv with='v_iv_0'' 
790124     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 69: 'rule impLeft' 
790125     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 70: 'tryclose branch' 
790261     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 71: 'rule getOfSwap' 
790263     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 72: 'rule ifthenelse_negated' 
790264     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 73: 'rule ifthenelse_split occ=0' 
790266     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 74: 'rule andLeft' 
790266     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 75: 'rule andLeft' 
790267     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 76: 'rule andLeft' 
790268     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 77: 'rule ifthenelse_split occ=0' 
790269     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 78: 'tryclose branch' 
790377     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 79: 'rule ifthenelse_split occ=0' 
790379     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 80: 'tryclose branch' 
790517     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 81: 'tryclose branch' 
790525     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 82: 'tryclose branch' 
790532     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 83: 'rule getOfSwap' 
790534     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 84: 'rule ifthenelse_negated' 
790535     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 85: 'rule ifthenelse_split occ=0' 
790536     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 86: 'rule andLeft' 
790537     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 87: 'rule andLeft' 
790538     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 88: 'rule andLeft' 
790538     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 89: 'rule ifthenelse_split occ=0' 
790540     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 90: 'tryclose branch' 
790552     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 91: 'tryclose branch' 
790559     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 92: 'tryclose branch' 
790700     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 93: 'rule getOfSwap' 
790702     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 94: 'rule ifthenelse_negated' 
790704     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 95: 'rule ifthenelse_split occ=0' 
790706     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 96: 'rule andLeft' 
790706     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 97: 'rule andLeft' 
790707     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 98: 'rule andLeft' 
790708     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 99: 'rule ifthenelse_split occ=0' 
790709     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 100: 'tryclose branch' 
790778     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 101: 'tryclose branch' 
790786     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 102: 'tryclose branch' 
790910     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 103: 'cut '(int)s_0[v_x_0] = (int)s_0[v_y_0]'' 
790913     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 104: 'rule seqNPermInjective' 
790916     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 105: 'instantiate hide var=iv with='v_x_0'' 
790918     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 106: 'instantiate hide var=jv with='v_y_0'' 
790919     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 107: 'rule impLeft' 
790920     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 108: 'tryclose branch' 
791084     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 109: 'tryclose branch' 
791089     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 110: 'cut '(int)s_0[v_x_0] = v_x_0'' 
791092     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)'' 
791094     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 112: 'rule andRight' 
791096     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 113: 'rule andRight' 
791100     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 114: 'rule andRight' 
791102     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 115: 'rule andRight' 
791103     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 116: 'tryclose branch' 
791113     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 117: 'rule seqNPermSwapNPerm' 
791120     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 118: 'instantiate hide var=iv with='v_y_0'' 
791123     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 119: 'instantiate hide var=jv with='jv_1'' 
791124     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 120: 'tryclose branch' 
791242     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 121: 'rule allRight' 
791244     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 122: 'rule impRight' 
791245     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 123: 'rule andLeft' 
791246     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 124: 'instantiate var=iv with='v_iv_0'' 
791248     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 125: 'rule impLeft' 
791250     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 126: 'tryclose branch' 
791410     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 127: 'rule getOfSwap' 
791413     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 128: 'rule ifthenelse_negated' 
791415     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 129: 'rule ifthenelse_split occ=0' 
791417     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 130: 'rule andLeft' 
791418     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 131: 'rule andLeft' 
791419     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 132: 'rule andLeft' 
791419     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 133: 'rule ifthenelse_split occ=0' 
791421     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 134: 'tryclose branch' 
791527     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 135: 'rule ifthenelse_split occ=0' 
791529     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 136: 'tryclose branch' 
791625     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 137: 'instantiate var=iv with='v_y_0'' 
791626     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 138: 'rule impLeft' 
791627     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 139: 'tryclose branch' 
791632     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 140: 'tryclose branch' 
791637     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 141: 'tryclose branch' 
791642     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 142: 'tryclose branch' 
791797     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 143: 'rule getOfSwap' 
791799     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 144: 'rule ifthenelse_negated' 
791800     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 145: 'rule ifthenelse_split occ=0' 
791802     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 146: 'tryclose branch' 
791814     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 147: 'tryclose branch' 
791959     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 148: 'tryclose branch' 
796279     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 149: 'cut  '(int)s_0[v_y_0] = v_y_0'' 
796281     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)'' 
796287     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 151: 'rule andRight' 
796289     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 152: 'rule andRight' 
796290     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 153: 'rule andRight' 
796290     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 154: 'rule andRight' 
796291     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 155: 'tryclose branch' 
796301     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 156: 'rule seqNPermSwapNPerm' 
796302     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 157: 'instantiate hide var=iv with='v_x_0'' 
796304     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 158: 'instantiate hide var=jv with='jv_0'' 
796305     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 159: 'rule impLeft' 
796305     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 160: 'tryclose branch' 
796419     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 161: 'tryclose branch' 
796424     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 162: 'rule allRight' 
796425     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 163: 'rule impRight' 
796426     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 164: 'rule andLeft' 
796427     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 165: 'instantiate var=iv with='v_iv_0'' 
796428     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 166: 'rule impLeft' 
796429     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 167: 'tryclose branch' 
796544     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 168: 'rule getOfSwap' 
796546     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 169: 'rule ifthenelse_negated' 
796547     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 170: 'rule ifthenelse_split occ=0' 
796549     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 171: 'rule andLeft' 
796549     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 172: 'rule andLeft' 
796550     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 173: 'rule andLeft' 
796551     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 174: 'rule ifthenelse_split occ=0' 
796553     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 175: 'tryclose branch' 
796648     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 176: 'rule ifthenelse_split occ=0' 
796649     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 177: 'tryclose branch' 
796746     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 178: 'tryclose branch' 
796752     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 179: 'tryclose branch' 
796757     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 180: 'rule getOfSwap' 
796758     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 181: 'rule ifthenelse_negated' 
796759     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 182: 'rule ifthenelse_split occ=0' 
796761     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 183: 'tryclose branch' 
796773     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 184: 'tryclose branch' 
796873     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 185: 'rule getOfSwap' 
796874     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 186: 'rule ifthenelse_negated' 
796876     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 187: 'rule ifthenelse_split occ=0' 
796877     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 188: 'tryclose branch' 
796965     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 189: 'tryclose branch' 
796977     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 190: 'cut '(int)s_0[v_x_0]=v_y_0'' 
796978     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)'' 
796980     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 192: 'rule andRight' 
796982     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 193: 'rule andRight' 
796983     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 194: 'rule andRight' 
796983     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 195: 'rule andRight' 
796984     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 196: 'tryclose branch' 
796997     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 197: 'rule seqNPermSwapNPerm' 
796999     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 198: 'instantiate hide var=iv with='jv_0'' 
797000     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 199: 'instantiate hide var=jv with='v_x_0'' 
797001     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 200: 'rule impLeft' 
797002     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 201: 'tryclose branch' 
797108     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 202: 'rule seqNPermSwapNPerm formula='seqNPerm(seqSwap(s_0, jv_0, v_x_0))'' 
797110     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 203: 'instantiate hide var=iv with='jv_0'' 
797112     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 204: 'instantiate hide var=jv with='v_y_0'' 
797113     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 205: 'rule impLeft' 
797114     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 206: 'tryclose branch' 
797236     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 207: 'tryclose branch' 
797242     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 208: 'rule allRight' 
797243     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 209: 'rule impRight' 
797243     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 210: 'rule andLeft' 
797244     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 211: 'instantiate var=iv with='v_iv_0'' 
797245     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 212: 'rule impLeft' 
797245     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 213: 'tryclose branch' 
797371     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 214: 'rule getOfSwap' 
797373     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 215: 'rule ifthenelse_negated' 
797374     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 216: 'rule ifthenelse_split occ=0' 
797375     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 217: 'rule andLeft' 
797376     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 218: 'rule andLeft' 
797376     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 219: 'rule andLeft' 
797377     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 220: 'rule ifthenelse_split occ=0' 
797378     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 221: 'rule getOfSwap' 
797379     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 222: 'rule ifthenelse_negated' 
797380     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 223: 'rule ifthenelse_split occ=0' 
797381     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 224: 'rule andLeft' 
797381     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 225: 'rule andLeft' 
797382     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 226: 'rule andLeft' 
797382     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 227: 'rule ifthenelse_split occ=0' 
797383     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 228: 'tryclose branch' 
797492     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 229: 'rule ifthenelse_split occ=0' 
797494     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 230: 'tryclose branch' 
797552     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 231: 'tryclose branch' 
797644     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 232: 'tryclose branch' 
797739     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 233: 'rule ifthenelse_split' 
797741     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 234: 'rule getOfSwap' 
797742     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 235: 'rule ifthenelse_negated' 
797742     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 236: 'rule ifthenelse_split occ=0' 
797743     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 237: 'rule andLeft' 
797744     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 238: 'rule andLeft' 
797744     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 239: 'rule andLeft' 
797744     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 240: 'rule ifthenelse_split occ=0' 
797746     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 241: 'tryclose branch' 
797848     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 242: 'tryclose branch' 
797855     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 243: 'tryclose branch' 
797962     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 244: 'rule getOfSwap' 
797964     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 245: 'rule ifthenelse_negated' 
797965     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 246: 'rule ifthenelse_split occ=0' 
797967     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 247: 'rule andLeft' 
797967     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 248: 'rule andLeft' 
797968     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 249: 'rule andLeft' 
797969     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 250: 'rule ifthenelse_split occ=0' 
797970     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 251: 'tryclose branch' 
797976     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 252: 'rule ifthenelse_split occ=0' 
797977     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 253: 'tryclose branch' 
798073     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 254: 'tryclose branch' 
798079     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 255: 'tryclose branch' 
798085     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 256: 'tryclose branch' 
798202     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 257: 'rule getOfSwap' 
798203     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 258: 'rule ifthenelse_negated' 
798204     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 259: 'rule ifthenelse_split occ=0' 
798205     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 260: 'rule andLeft' 
798206     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 261: 'rule andLeft' 
798206     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 262: 'rule andLeft' 
798206     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 263: 'rule ifthenelse_split occ=0' 
798207     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 264: 'tryclose branch' 
798272     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 265: 'rule ifthenelse_split occ=0' 
798273     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 266: 'rule getOfSwap' 
798274     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 267: 'rule ifthenelse_negated' 
798275     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 268: 'rule ifthenelse_split occ=0' 
798276     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 269: 'tryclose branch' 
798282     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 270: 'tryclose branch' 
798288     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 271: 'tryclose branch' 
798426     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 272: 'tryclose branch' 
798531     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 273: 'rule getOfSwap' 
798532     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 274: 'rule ifthenelse_negated' 
798533     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 275: 'rule ifthenelse_split occ=0' 
798534     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 276: 'tryclose branch' 
798731     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 277: 'tryclose branch' 
798836     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 278: 'cut 'int::seqGet(s_0, v_y_0)=v_x_0'' 
798837     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 279: 'tryclose branch' 
802600     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 280: 'rule seqNPermSwapNPerm' 
802606     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 281: 'instantiate hide var=iv with='jv_1'' 
802607     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 282: 'instantiate hide var=jv with='v_y_0'' 
802608     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 283: 'rule impLeft' 
802609     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 284: 'tryclose branch' 
802756     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 285: 'rule seqNPermSwapNPerm formula='seqNPerm(seqSwap(s_0,jv_1,v_y_0))'' 
802757     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 286: 'instantiate hide var=iv with='jv_1'' 
802758     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 287: 'instantiate hide var=jv with='v_x_0'' 
802759     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 288: 'rule impLeft' 
802760     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 289: 'tryclose branch' 
802892     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 290: 'tryclose branch' 
806727     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 291: 'tryclose branch' 
810591     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 292: 'rule seqNPermSwapNPerm formula='seqNPerm(s_0)'' 
810596     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 293: 'instantiate hide var=iv with='v_x_0'' 
810597     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 294: 'instantiate hide var=jv with='jv_0'' 
810598     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 295: 'rule impLeft' 
810599     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 296: 'tryclose branch' 
810734     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 297: 'rule seqNPermSwapNPerm formula='seqNPerm(seqSwap(s_0,v_x_0,jv_0))'' 
810736     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 298: 'instantiate hide var=iv with='v_y_0'' 
810737     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 299: 'instantiate hide var=jv with='jv_1'' 
810738     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)' ...' 
810740     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 301: 'tryclose branch' 
812135     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm2/Taclet_schiffl_thm_1.proof 
812135     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 93.81ns 
812136     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
815172     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.04s 
815172     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: schiffl_thm_1 
816143     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: schiffl_thm_1 
816145     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 8.1ns 
816145     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 1: 'macro split-prop' 
816154     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 2: 'rule schiffl_lemma_2 formula='seqPerm(f_s, f_t)'' 
816168     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 3: 'instantiate hide var=x with='f_x'' 
816171     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 4: 'instantiate hide var=y with='f_y'' 
816173     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 5: 'rule impLeft' 
816173     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 6: 'tryclose branch' 
816178     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 7: 'rule exLeft' 
816180     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 8: 'macro split-prop' 
816183     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 9: 'rule seqPermDef occ=1' 
816254     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 10: 'rule andRight' 
816255     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 11: 'tryclose branch' 
816265     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 12: 'instantiate hide var=s with='r_0'' 
816267     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 13: 'rule andRight' 
816269     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 14: 'tryclose branch' 
816319     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 15: 'rule allRight' 
816320     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 16: 'rule impRight' 
816321     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 17: 'instantiate hide var=iv with='iv_0'' 
816322     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 18: 'rule impLeft' 
816322     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 19: 'tryclose branch' 
816392     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 20: 'rule andLeft' 
816393     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 21: 'rule seqNPermRange' 
816394     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 22: 'instantiate hide var=iv with='iv_0'' 
816395     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 23: 'rule impLeft' 
816396     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 24: 'tryclose branch' 
816400     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 25: 'rule andLeft' 
816401     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 26: 'rule andLeft' 
816402     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 27: 'rule seqNPermRange' 
816403     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 28: 'instantiate hide var=iv with='f_x'' 
816404     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 29: 'rule impLeft' 
816405     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 30: 'tryclose branch' 
816491     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 31: 'rule andLeft' 
816492     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 32: 'rule andLeft' 
816492     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 33: 'rule seqNPermRange' 
816494     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 34: 'instantiate hide var=iv with='f_y'' 
816495     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 35: 'rule impLeft' 
816495     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 36: 'tryclose branch' 
816587     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 37: 'rule andLeft' 
816588     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 38: 'rule andLeft' 
816588     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 39: 'rule getOfSeqDef occ=0' 
816589     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 40: 'rule getOfSeqDef' 
816590     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 41: 'rule ifthenelse_split occ=0' 
816591     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 42: 'rule andLeft occ=0' 
816592     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 43: 'rule sub_zero_2 occ=0' 
816592     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 44: 'rule ifthenelse_split occ=2' 
816593     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 45: 'rule andLeft' 
816594     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 46: 'rule sub_zero_2 occ=0' 
816594     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 47: 'rule add_zero_right occ=0' 
816595     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 48: 'rule add_zero_right occ=0' 
816596     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 49: 'rule add_zero_right occ=0' 
816596     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 50: 'rule add_zero_right occ=0' 
816597     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 51: 'rule add_zero_right occ=0' 
816597     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 52: 'rule add_zero_right occ=0' 
816598     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 53: 'rule ifthenelse_split occ=0' 
816599     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 54: 'rule ifthenelse_split occ=0' 
816600     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 55: 'tryclose branch' 
816603     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 56: 'tryclose branch' 
816643     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 57: 'rule ifthenelse_split occ=0' 
816645     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 58: 'tryclose branch' 
816700     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 59: 'rule ifthenelse_split occ=0' 
816702     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 60: 'rule seqNPermInjective' 
816703     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 61: 'instantiate hide var=iv with='iv_0'' 
816705     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 62: 'instantiate hide var=jv with='f_y'' 
816706     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 63: 'rule impLeft' 
816706     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 64: 'tryclose branch' 
816755     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 65: 'tryclose branch' 
816758     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 66: 'rule ifthenelse_split occ=0' 
816760     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 67: 'rule seqNPermInjective' 
816761     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 68: 'instantiate hide var=iv with='iv_0'' 
816763     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 69: 'instantiate hide var=jv with='f_x'' 
816763     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 70: 'rule impLeft' 
816764     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 71: 'tryclose branch' 
816813     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 72: 'tryclose branch' 
816816     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 73: 'tryclose branch' 
816820     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 74: 'tryclose branch' 
816878     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 75: 'tryclose branch' 
816939     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_eqSameSeq.proof 
816939     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 132.81ns 
816940     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
819950     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.01s 
819951     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: eqSameSeq 
820975     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: eqSameSeq 
821012     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 33.26ms