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

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

tests
0

failures
0

ignored
13m0.97s

duration
100%

successful

Tests

Test Method name Duration Result
powPositive data()[100] 3.650s passed
powPositiveConcrete data()[101] 3.962s passed
powGeq1Concrete data()[102] 3.740s passed
pow2InIntLower data()[103] 3.814s passed
pow2InIntUpper data()[104] 3.746s passed
logSelfConcrete data()[105] 3.912s passed
log1Concrete data()[106] 3.812s passed
logProduct data()[107] 3.634s passed
logTimesBaseConcrete data()[108] 3.657s passed
logProdIdentity data()[109] 3.697s passed
moduloByteIsInByte data()[10] 3.884s passed
logProdIdentityConcrete data()[110] 3.829s passed
logPowIdentity data()[111] 3.809s passed
logPowIdentityConcrete data()[112] 3.872s passed
logPositive data()[113] 3.893s passed
logPositiveConcrete data()[114] 3.788s passed
logMono data()[115] 3.642s passed
logMonoConcrete data()[116] 3.620s passed
powLogLess data()[117] 3.843s passed
powLogMore2 data()[118] 3.905s passed
logLessThanPow data()[119] 3.941s passed
moduloCharIsInChar data()[11] 3.828s passed
logLessThanPowConcrete data()[120] 3.659s passed
logSqueeze data()[121] 3.724s passed
ifthenelse_equals data()[122] 3.710s passed
ifthenelse_equals_1 data()[123] 3.854s passed
ifthenelse_equals_2 data()[124] 3.733s passed
disjointWithSingleton1 data()[125] 3.947s passed
disjointWithSingleton2 data()[126] 3.824s passed
disjointArrayRanges data()[127] 3.838s passed
disjointArrayRangeAllFields1 data()[128] 3.913s passed
disjointArrayRangeAllFields2 data()[129] 3.795s passed
div_unique1 data()[12] 3.987s passed
seqSelfDefinition data()[130] 3.611s passed
seqOutsideValue data()[131] 3.678s passed
castedGetAny data()[132] 3.622s passed
seqGetAlphaCast data()[133] 3.788s passed
getOfSeqSingleton data()[134] 3.814s passed
getOfSeqSingletonConcrete data()[135] 3.612s passed
getOfSeqConcat data()[136] 3.762s passed
getOfSeqSub data()[137] 3.640s passed
getOfSeqReverse data()[138] 3.641s passed
lenOfSeqEmpty data()[139] 3.635s passed
div_unique2 data()[13] 3.785s passed
lenOfSeqSingleton data()[140] 3.755s passed
lenOfSeqConcat data()[141] 3.798s passed
lenOfSeqSub data()[142] 3.900s passed
lenOfSeqReverse data()[143] 3.800s passed
equalityToSeqGetAndSeqLenLeft data()[144] 3.606s passed
equalityToSeqGetAndSeqLenRight data()[145] 3.764s passed
getOfSeqSingletonEQ data()[146] 3.840s passed
getOfSeqConcatEQ data()[147] 3.827s passed
getOfSeqSubEQ data()[148] 3.856s passed
getOfSeqReverseEQ data()[149] 3.922s passed
div_exists data()[14] 3.934s passed
lenOfSeqEmptyEQ data()[150] 3.877s passed
lenOfSeqSingletonEQ data()[151] 4.071s passed
lenOfSeqConcatEQ data()[152] 3.729s passed
lenOfSeqSubEQ data()[153] 3.683s passed
lenOfSeqReverseEQ data()[154] 3.760s passed
getOfSeqDefEQ data()[155] 3.997s passed
lenOfSeqDefEQ data()[156] 3.761s passed
seqConcatWithSeqEmpty1 data()[157] 3.908s passed
seqConcatWithSeqEmpty2 data()[158] 3.673s passed
seqReverseOfSeqEmpty data()[159] 3.606s passed
div_one data()[15] 3.724s passed
subSeqComplete data()[160] 3.622s passed
subSeqTailR data()[161] 3.903s passed
subSeqTailL data()[162] 3.816s passed
subSeqTailEQR data()[163] 3.694s passed
subSeqTailEQL data()[164] 3.890s passed
seqDef_split data()[165] 3.895s passed
seqDef_induction_upper data()[166] 3.820s passed
seqDef_induction_upper_concrete data()[167] 3.989s passed
seqDef_induction_lower data()[168] 4.047s passed
seqDef_induction_lower_concrete data()[169] 4.008s passed
jdiv_one data()[16] 3.829s passed
seqDef_split_in_three data()[170] 3.946s passed
seqDef_empty data()[171] 3.689s passed
seqDef_one_summand data()[172] 3.690s passed
seqDef_lower_equals_upper data()[173] 3.810s passed
seqDefOfSeq data()[174] 3.917s passed
seqSelfDefinitionEQ2 data()[175] 3.973s passed
indexOfSeqSingleton data()[176] 3.844s passed
indexOfSeqConcatFirst data()[177] 3.818s passed
indexOfSeqConcatSecond data()[178] 3.890s passed
indexOfSeqSub data()[179] 3.932s passed
div_zero data()[17] 3.948s passed
lenOfArray2seq data()[180] 3.931s passed
getAnyOfArray2seq data()[181] 3.654s passed
getOfArray2seq data()[182] 3.681s passed
getAnyOfNPermInv data()[183] 3.925s passed
seqNPermRange data()[184] 3.895s passed
seqPermTrans data()[185] 3.980s passed
seqPermRefl data()[186] 4.038s passed
seqPermSplit data()[187] 3.946s passed
seqNPermRight data()[188] 4.201s passed
seqPermFromSwap data()[189] 4.023s passed
divResZero1 data()[18] 3.730s passed
seqPermTransAlt0 data()[190] 3.856s passed
seqPermTransAlt1 data()[191] 3.872s passed
seqPermTransAlt2 data()[192] 3.897s passed
seqPermTransAlt3 data()[193] 3.821s passed
seqPermForall data()[194] 3.930s passed
seqPermExists data()[195] 3.981s passed
schiffl_lemma_2 data()[196] 27.116s passed
schiffl_thm_1 data()[197] 4.766s passed
eqSameSeq data()[198] 3.991s passed
divResZero2 data()[19] 3.881s passed
eqTermCut data()[1] 4.453s passed
divResOne1 data()[20] 3.893s passed
divResOne2 data()[21] 3.656s passed
div_cancel1 data()[22] 3.689s passed
div_cancel2 data()[23] 3.669s passed
divAddMultDenom data()[24] 3.723s passed
divMinus data()[25] 3.728s passed
divMinusDenom data()[26] 3.849s passed
divLeastDPos data()[27] 3.705s passed
divLeastDNeg data()[28] 3.916s passed
divGreatestDPos data()[29] 4.015s passed
equivAllRight data()[2] 4.093s passed
divGreatestDNeg data()[30] 3.674s passed
divIncreasingPos data()[31] 3.852s passed
divIncreasingNeg data()[32] 3.917s passed
jdiv_zero data()[33] 3.688s passed
jdivPulloutMinusNum data()[34] 3.980s passed
jdivPulloutMinusDenom data()[35] 3.753s passed
jdiv_uniquePosPos data()[36] 3.853s passed
jdiv_uniquePosNeg data()[37] 3.735s passed
jdiv_uniqueNegPos data()[38] 3.947s passed
jdiv_uniqueNegNeg data()[39] 3.935s passed
irrflConcrete1 data()[3] 4.344s passed
jdivMultDenom1 data()[40] 3.798s passed
jdivMultDenom2 data()[41] 3.672s passed
mod_geZero data()[42] 3.681s passed
mod_lessDenom data()[43] 3.937s passed
jmod_NumPos data()[44] 3.874s passed
jmod_NumNeg data()[45] 3.665s passed
jmod_geZero data()[46] 3.711s passed
jmodNumZero data()[47] 3.894s passed
jmod_pulloutminusNum data()[48] 3.892s passed
jmod_pulloutminusDenom data()[49] 3.800s passed
irrflConcrete2 data()[4] 4.414s passed
jmodUnique1 data()[50] 3.895s passed
jmodUnique2 data()[51] 3.994s passed
intDivRem data()[52] 3.663s passed
jmodjmod data()[53] 3.824s passed
jmodDivisible data()[54] 3.831s passed
jmodDivisibleRep data()[55] 3.676s passed
jdivAddMultDenom data()[56] 3.952s passed
jmodAltZero data()[57] 3.663s passed
jmodAddMultDenomZero data()[58] 3.645s passed
polyDiv_zero data()[59] 3.665s passed
cancel_gtPos data()[5] 3.905s passed
polyMod_ltdivDenom data()[60] 3.667s passed
bsum_empty data()[61] 3.654s passed
bsum_induction_upper data()[62] 3.629s passed
bsum_induction_lower data()[63] 3.722s passed
bsum_num_of_bounds data()[64] 3.773s passed
bsum_num_of_bounds2 data()[65] 3.879s passed
bsum_induction_upper2 data()[66] 3.665s passed
bsum_induction_upper_concrete data()[67] 3.668s passed
bsum_induction_upper_concrete_2 data()[68] 3.674s passed
bsum_induction_upper2_concrete data()[69] 3.631s passed
cancel_gtNeg data()[6] 3.803s passed
bsum_induction_lower_concrete data()[70] 3.629s passed
bsum_induction_lower2 data()[71] 3.648s passed
bsum_induction_lower2_concrete data()[72] 3.676s passed
bsum_positive data()[73] 3.894s passed
bsum_upper_bound data()[74] 3.786s passed
bsum_lower_bound data()[75] 3.807s passed
bsum_positive_lower_bound_element data()[76] 4.016s passed
bsum_sub_same_index data()[77] 3.920s passed
bsum_less_same_index data()[78] 3.829s passed
bsum_equal_except_one_index data()[79] 3.704s passed
moduloIntIsInInt data()[7] 3.802s passed
bsum_num_of_is_max data()[80] 3.795s passed
bsum_num_of_is_max2 data()[81] 3.722s passed
bsum_num_of_is_max3 data()[82] 3.904s passed
bsum_num_of_is_max4 data()[83] 3.896s passed
bsum_num_of_lt_max data()[84] 3.990s passed
bsum_num_of_lt_max2 data()[85] 3.878s passed
bsum_num_of_lt_max3 data()[86] 3.868s passed
bsum_num_of_lt_max4 data()[87] 3.913s passed
bsum_num_of_gt0 data()[88] 3.914s passed
bsum_num_of_gt0_alt data()[89] 3.647s passed
moduloLongIsInLong data()[8] 3.714s passed
bsum_add_concrete data()[90] 3.797s passed
bprod_all_positive data()[91] 3.903s passed
bprod_split data()[92] 3.941s passed
powConcrete0 data()[93] 3.859s passed
powConcrete1 data()[94] 3.916s passed
powSplitFactor data()[95] 3.765s passed
powAdd data()[96] 3.888s passed
powMono data()[97] 3.748s passed
powMonoConcrete data()[98] 3.892s passed
powMonoConcreteRight data()[99] 3.656s passed
moduloShortIsInShort data()[9] 3.841s passed

Standard output

465        INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src/test/resources/testcase/dummyTrue.key 
539        DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 27.39ms 
896        INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
919        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)

2133       DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for Meta 
2135       DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for Meta 
2138       DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for Meta 
2138       DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for Meta 
4184       DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for JavaBigintExpression 
10614      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 9.72s 
10694      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof dummyTrue.key 
10738      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 42.5ns 
10758      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/firstOrder/Taclet_eqTermCut.proof 
10759      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 777.51ns 
10768      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
14102      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.33s 
14105      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: eqTermCut 
15154      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: eqTermCut 
15196      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 25.26ms 
15212      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/firstOrder/Taclet_equivAllRight.proof 
15213      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 515.61ns 
15215      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
18267      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.05s 
18268      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: equivAllRight 
19285      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: equivAllRight 
19301      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 12.05ms 
19305      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_irrflConcrete1.proof 
19306      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 441.11ns 
19307      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
22525      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.22s 
22526      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: irrflConcrete1 
23638      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: irrflConcrete1 
23646      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.26ms 
23650      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_irrflConcrete2.proof 
23650      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 513.01ns 
23652      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
26958      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.31s 
26959      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: irrflConcrete2 
28043      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: irrflConcrete2 
28060      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 11.05ms 
28067      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_cancel_gtPos.proof 
28068      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 949.31ns 
28069      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
30982      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.91s 
30983      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: cancel_gtPos 
31923      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: cancel_gtPos 
31968      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 41.79ms 
31972      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_cancel_gtNeg.proof 
31974      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 1.44ms 
31975      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
34815      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.84s 
34816      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: cancel_gtNeg 
35750      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: cancel_gtNeg 
35772      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 18.77ms 
35776      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intRulesIgnoringOF/Taclet_moduloIntIsInInt.proof 
35777      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 400.21ns 
35778      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
38637      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.86s 
38637      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: moduloIntIsInInt 
39572      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: moduloIntIsInInt 
39576      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 906.62ns 
39579      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intRulesIgnoringOF/Taclet_moduloLongIsInLong.proof 
39580      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 435.51ns 
39581      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
42357      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.78s 
42357      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: moduloLongIsInLong 
43287      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: moduloLongIsInLong 
43290      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 644.91ns 
43293      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intRulesIgnoringOF/Taclet_moduloShortIsInShort.proof 
43293      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 144ns 
43294      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
46130      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.84s 
46131      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: moduloShortIsInShort 
47127      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: moduloShortIsInShort 
47131      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 668.21ns 
47134      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intRulesIgnoringOF/Taclet_moduloByteIsInByte.proof 
47134      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 357.01ns 
47135      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
49988      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.85s 
49989      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: moduloByteIsInByte 
51011      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: moduloByteIsInByte 
51016      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 701.31ns 
51020      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intRulesIgnoringOF/Taclet_moduloCharIsInChar.proof 
51022      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 1.67ms 
51024      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
53912      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.89s 
53912      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: moduloCharIsInChar 
54842      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: moduloCharIsInChar 
54845      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 673.61ns 
54857      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_div_unique1.proof 
54857      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 482.31ns 
54859      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
57871      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.01s 
57872      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: div_unique1 
58792      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: div_unique1 
58840      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 42.74ms 
58847      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_div_unique2.proof 
58848      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 787.51ns 
58849      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
61663      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.81s 
61663      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: div_unique2 
62586      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: div_unique2 
62628      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 38.13ms 
62632      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_div_exists.proof 
62632      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 390.51ns 
62634      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
65407      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.77s 
65407      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: div_exists 
66332      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: div_exists 
66562      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 219ms 
66566      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_div_one.proof 
66567      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 432.91ns 
66568      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
69346      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.78s 
69347      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: div_one 
70276      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: div_one 
70287      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 6.79ms 
70292      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdiv_one.proof 
70292      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 334.5ns 
70294      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
73192      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.9s 
73193      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdiv_one 
74114      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdiv_one 
74118      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.45ms 
74121      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_div_zero.proof 
74122      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 397.81ns 
74123      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
76954      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.83s 
76954      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: div_zero 
77988      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: div_zero 
78067      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 73.62ms 
78069      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divResZero1.proof 
78069      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 149.2ns 
78071      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
80865      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.79s 
80865      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divResZero1 
81780      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divResZero1 
81797      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 13.81ms 
81798      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divResZero2.proof 
81798      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 109.6ns 
81799      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
84632      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.83s 
84633      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divResZero2 
85660      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divResZero2 
85677      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 13.61ms 
85681      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divResOne1.proof 
85681      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 380.41ns 
85683      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
88623      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.94s 
88624      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divResOne1 
89553      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divResOne1 
89570      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 14.4ms 
89573      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divResOne2.proof 
89574      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 361.7ns 
89575      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
92291      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.72s 
92291      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divResOne2 
93210      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divResOne2 
93227      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 13.3ms 
93228      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_div_cancel1.proof 
93229      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 125.4ns 
93230      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
95964      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.73s 
95965      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: div_cancel1 
96888      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: div_cancel1 
96916      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 23.93ms 
96919      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_div_cancel2.proof 
96919      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 394.11ns 
96920      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
99664      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.74s 
99665      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: div_cancel2 
100577     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: div_cancel2 
100584     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 5.06ms 
100587     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divAddMultDenom.proof 
100588     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 356.7ns 
100590     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
103348     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.76s 
103349     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divAddMultDenom 
104262     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divAddMultDenom 
104308     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 39.67ms 
104309     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divMinus.proof 
104310     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 118.2ns 
104311     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
107078     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.77s 
107079     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divMinus 
107966     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divMinus 
108036     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 62.96ms 
108040     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divMinusDenom.proof 
108040     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 694.11ns 
108042     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
110876     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.83s 
110876     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divMinusDenom 
111809     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divMinusDenom 
111885     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 68.9ms 
111892     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divLeastDPos.proof 
111895     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 2.87ms 
111897     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
114687     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.79s 
114687     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divLeastDPos 
115583     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divLeastDPos 
115592     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 6.62ms 
115596     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divLeastDNeg.proof 
115596     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 144.8ns 
115597     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
118524     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.93s 
118524     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divLeastDNeg 
119481     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divLeastDNeg 
119509     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 22.77ms 
119511     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divGreatestDPos.proof 
119511     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 139.3ns 
119517     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
122625     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.11s 
122625     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divGreatestDPos 
123510     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divGreatestDPos 
123524     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 10.98ms 
123525     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divGreatestDNeg.proof 
123526     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 133.7ns 
123526     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
126304     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.78s 
126305     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divGreatestDNeg 
127190     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divGreatestDNeg 
127199     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 6.55ms 
127200     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divIncreasingPos.proof 
127200     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 130.2ns 
127201     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
130091     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.89s 
130092     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divIncreasingPos 
131041     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divIncreasingPos 
131050     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 6.65ms 
131052     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divIncreasingNeg.proof 
131052     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 189.7ns 
131053     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
134013     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.96s 
134013     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divIncreasingNeg 
134956     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divIncreasingNeg 
134966     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 7.99ms 
134970     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdiv_zero.proof 
134970     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 443.21ns 
134971     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
137769     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.8s 
137769     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdiv_zero 
138651     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdiv_zero 
138656     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.74ms 
138657     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdivPulloutMinusNum.proof 
138657     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 113.9ns 
138658     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
141614     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.96s 
141614     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdivPulloutMinusNum 
142583     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdivPulloutMinusNum 
142635     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 49.27ms 
142638     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdivPulloutMinusDenom.proof 
142638     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 359.9ns 
142639     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
145412     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.77s 
145413     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdivPulloutMinusDenom 
146322     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdivPulloutMinusDenom 
146387     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 58.95ms 
146400     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdiv_uniquePosPos.proof 
146400     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 442.61ns 
146401     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
149283     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.88s 
149283     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdiv_uniquePosPos 
150211     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdiv_uniquePosPos 
150241     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 22.37ms 
150244     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdiv_uniquePosNeg.proof 
150244     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 322.2ns 
150246     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
153003     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.76s 
153004     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdiv_uniquePosNeg 
153954     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdiv_uniquePosNeg 
153977     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 19.61ms 
153978     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdiv_uniqueNegPos.proof 
153979     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 202.5ns 
153981     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
156938     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.96s 
156938     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdiv_uniqueNegPos 
157903     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdiv_uniqueNegPos 
157924     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 17.62ms 
157926     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdiv_uniqueNegNeg.proof 
157926     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 147.8ns 
157927     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
160883     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.96s 
160883     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdiv_uniqueNegNeg 
161839     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdiv_uniqueNegNeg 
161859     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 17.06ms 
161861     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdivMultDenom1.proof 
161861     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 123.4ns 
161862     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
164643     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.78s 
164644     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdivMultDenom1 
165612     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdivMultDenom1 
165657     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 39.63ms 
165659     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdivMultDenom2.proof 
165659     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 101.2ns 
165660     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
168406     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.75s 
168406     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdivMultDenom2 
169327     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdivMultDenom2 
169330     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.14ms 
169331     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_mod_geZero.proof 
169331     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 90.3ns 
169332     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
172086     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.75s 
172086     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: mod_geZero 
173005     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: mod_geZero 
173010     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.86ms 
173012     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_mod_lessDenom.proof 
173012     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 128.7ns 
173013     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
175951     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.94s 
175952     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: mod_lessDenom 
176936     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: mod_lessDenom 
176946     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 6.55ms 
176949     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmod_NumPos.proof 
176949     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 328.6ns 
176950     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
179884     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.93s 
179884     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmod_NumPos 
180811     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmod_NumPos 
180821     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 7.48ms 
180822     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmod_NumNeg.proof 
180822     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 103.8ns 
180823     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
183554     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.73s 
183554     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmod_NumNeg 
184465     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmod_NumNeg 
184487     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 18.39ms 
184488     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmod_geZero.proof 
184488     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 120.9ns 
184489     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
187219     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.73s 
187219     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmod_geZero 
188183     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmod_geZero 
188197     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 10.38ms 
188199     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmodNumZero.proof 
188199     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 137ns 
188200     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
191095     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.89s 
191095     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmodNumZero 
192084     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmodNumZero 
192090     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.93ms 
192099     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmod_pulloutminusNum.proof 
192100     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 380.8ns 
192101     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
194992     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.89s 
194993     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmod_pulloutminusNum 
195980     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmod_pulloutminusNum 
195986     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.26ms 
195987     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmod_pulloutminusDenom.proof 
195987     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 127.5ns 
195988     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
198862     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.87s 
198862     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmod_pulloutminusDenom 
199781     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmod_pulloutminusDenom 
199786     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.33ms 
199787     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmodUnique1.proof 
199787     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 129.7ns 
199788     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
202634     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.85s 
202634     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmodUnique1 
203591     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmodUnique1 
203680     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 79.38ms 
203682     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmodUnique2.proof 
203682     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 193.8ns 
203684     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
206583     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.9s 
206584     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmodUnique2 
207573     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmodUnique2 
207674     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 88.55ms 
207676     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_intDivRem.proof 
207676     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 213.3ns 
207677     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
210421     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.74s 
210421     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: intDivRem 
211333     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: intDivRem 
211337     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.1ms 
211339     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmodjmod.proof 
211339     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 108.6ns 
211340     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
214120     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.78s 
214121     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmodjmod 
215082     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmodjmod 
215159     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 68.74ms 
215163     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmodDivisible.proof 
215169     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 6.04ms 
215171     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
218051     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.88s 
218052     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmodDivisible 
218957     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmodDivisible 
218992     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 30.65ms 
218994     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmodDivisibleRep.proof 
218994     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 103.4ns 
218995     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
221778     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.78s 
221779     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmodDivisibleRep 
222665     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmodDivisibleRep 
222668     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.35ms 
222670     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdivAddMultDenom.proof 
222670     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 93.8ns 
222671     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
225470     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.8s 
225470     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdivAddMultDenom 
226434     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdivAddMultDenom 
226619     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 167.97ms 
226622     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmodAltZero.proof 
226622     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 286.3ns 
226623     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
229386     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.76s 
229387     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmodAltZero 
230270     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmodAltZero 
230283     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 10.91ms 
230284     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmodAddMultDenomZero.proof 
230285     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 98.8ns 
230285     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
233040     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.75s 
233040     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmodAddMultDenomZero 
233918     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmodAddMultDenomZero 
233928     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 7.23ms 
233929     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_polyDiv_zero.proof 
233929     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 85.2ns 
233930     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
236690     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.76s 
236690     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: polyDiv_zero 
237573     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: polyDiv_zero 
237593     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 17.39ms 
237595     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_polyMod_ltdivDenom.proof 
237595     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 86ns 
237596     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
240362     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.77s 
240362     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: polyMod_ltdivDenom 
241243     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: polyMod_ltdivDenom 
241259     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 7.6ms 
241262     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_empty.proof 
241262     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 122.1ns 
241263     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
244030     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.77s 
244030     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_empty 
244910     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_empty 
244914     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.9ms 
244915     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_induction_upper.proof 
244915     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 80.4ns 
244916     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
247658     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.74s 
247658     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_upper 
248538     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_induction_upper 
248544     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.34ms 
248545     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_induction_lower.proof 
248545     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 76.9ns 
248546     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
251313     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.77s 
251313     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_lower 
252193     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_induction_lower 
252265     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 68.14ms 
252268     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_bounds.proof 
252268     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 305.31ns 
252269     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
255042     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.77s 
255043     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_bounds 
256015     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_bounds 
256038     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 18.96ms 
256039     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_bounds2.proof 
256039     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 102.4ns 
256040     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
258992     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.95s 
258992     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_bounds2 
259898     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_bounds2 
259917     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 16.16ms 
259918     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_induction_upper2.proof 
259919     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 86.9ns 
259919     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
262658     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.74s 
262658     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_upper2 
263578     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_induction_upper2 
263582     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.99ms 
263584     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_induction_upper_concrete.proof 
263584     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 90.9ns 
263585     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
266316     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.73s 
266316     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_upper_concrete 
267245     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_induction_upper_concrete 
267250     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.3ms 
267252     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_induction_upper_concrete_2.proof 
267252     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 91.9ns 
267253     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
270011     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.76s 
270011     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_upper_concrete_2 
270917     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_induction_upper_concrete_2 
270924     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.42ms 
270925     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_induction_upper2_concrete.proof 
270926     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 104.6ns 
270926     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
273647     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.72s 
273648     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_upper2_concrete 
274552     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_induction_upper2_concrete 
274555     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.65ms 
274557     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_induction_lower_concrete.proof 
274557     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 90.9ns 
274558     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
277277     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.72s 
277277     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_lower_concrete 
278182     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_induction_lower_concrete 
278185     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 878.62ns 
278186     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_induction_lower2.proof 
278186     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 70.1ns 
278187     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
280913     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.73s 
280913     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_lower2 
281827     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_induction_lower2 
281832     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.72ms 
281834     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_induction_lower2_concrete.proof 
281834     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 107.1ns 
281835     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
284601     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.77s 
284601     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_lower2_concrete 
285505     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_induction_lower2_concrete 
285508     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.18ms 
285509     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_positive.proof 
285509     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 68.3ns 
285510     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
288412     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.9s 
288412     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_positive 
289349     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_positive 
289402     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 49.3ms 
289404     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_upper_bound.proof 
289404     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 248.1ns 
289405     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
292188     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.78s 
292189     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_upper_bound 
293149     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_upper_bound 
293188     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 35.64ms 
293190     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_lower_bound.proof 
293190     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 77.2ns 
293191     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
295979     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.79s 
295979     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_lower_bound 
296947     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_lower_bound 
296995     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 44.08ms 
296999     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_positive_lower_bound_element.proof 
296999     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 331.2ns 
297000     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
299954     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.95s 
299955     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_positive_lower_bound_element 
300951     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_positive_lower_bound_element 
301011     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 54.65ms 
301012     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_sub_same_index.proof 
301012     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 77.2ns 
301013     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
303930     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.92s 
303930     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_sub_same_index 
304895     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_sub_same_index 
304932     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 32.81ms 
304933     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_less_same_index.proof 
304933     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 90.9ns 
304934     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
307722     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.79s 
307723     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_less_same_index 
308697     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_less_same_index 
308759     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 56ms 
308762     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_equal_except_one_index.proof 
308762     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 154.8ns 
308763     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
311471     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.71s 
311471     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_equal_except_one_index 
312427     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_equal_except_one_index 
312464     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 33.15ms 
312465     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_is_max.proof 
312465     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 103.2ns 
312467     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
315328     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.86s 
315329     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_is_max 
316236     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_is_max 
316260     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 20.47ms 
316261     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_is_max2.proof 
316261     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 90.4ns 
316262     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
318979     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.72s 
318980     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_is_max2 
319949     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_is_max2 
319981     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 27.98ms 
319983     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_is_max3.proof 
319983     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 142.6ns 
319984     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
322888     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.9s 
322888     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_is_max3 
323857     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_is_max3 
323885     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 24.4ms 
323887     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_is_max4.proof 
323887     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 129ns 
323889     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
326802     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.91s 
326802     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_is_max4 
327723     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_is_max4 
327781     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 54.46ms 
327784     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_lt_max.proof 
327784     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 283.3ns 
327785     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
330774     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.99s 
330774     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_lt_max 
331733     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_lt_max 
331771     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 34.01ms 
331772     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_lt_max2.proof 
331773     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 98.7ns 
331773     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
334658     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.88s 
334659     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_lt_max2 
335614     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_lt_max2 
335648     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 29.87ms 
335651     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_lt_max3.proof 
335651     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 274.5ns 
335653     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
338551     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.9s 
338552     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_lt_max3 
339487     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_lt_max3 
339517     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 26.21ms 
339518     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_lt_max4.proof 
339519     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 94.6ns 
339519     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
342452     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.93s 
342453     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_lt_max4 
343405     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_lt_max4 
343431     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 22.28ms 
343432     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_gt0.proof 
343432     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 78.4ns 
343433     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
346323     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.89s 
346323     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_gt0 
347311     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_gt0 
347344     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 30.17ms 
347347     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_gt0_alt.proof 
347347     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 270.8ns 
347348     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
350091     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.74s 
350091     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_gt0_alt 
350963     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_gt0_alt 
350991     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 25.3ms 
350993     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_add_concrete.proof 
350993     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 93.5ns 
350993     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
353807     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.81s 
353807     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_add_concrete 
354778     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_add_concrete 
354788     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 7.2ms 
354790     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bprod/Taclet_bprod_all_positive.proof 
354790     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 83.8ns 
354791     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
357699     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.91s 
357699     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bprod_all_positive 
358631     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bprod_all_positive 
358691     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 56.8ms 
358693     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bprod/Taclet_bprod_split.proof 
358693     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 63.2ns 
358694     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
361637     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.94s 
361637     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bprod_split 
362627     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bprod_split 
362633     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.86ms 
362634     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powConcrete0.proof 
362634     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 79ns 
362635     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
365531     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.9s 
365532     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powConcrete0 
366488     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powConcrete0 
366491     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 819.31ns 
366493     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powConcrete1.proof 
366493     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 72.7ns 
366494     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
369426     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.93s 
369426     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powConcrete1 
370404     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powConcrete1 
370407     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.3ms 
370409     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powSplitFactor.proof 
370409     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 61.7ns 
370409     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
373254     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.84s 
373254     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powSplitFactor 
374164     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powSplitFactor 
374172     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 5.56ms 
374174     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powAdd.proof 
374174     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 77.6ns 
374174     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
377056     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.88s 
377056     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powAdd 
378052     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powAdd 
378060     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.69ms 
378062     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powMono.proof 
378062     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 289.2ns 
378064     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
380869     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.81s 
380870     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powMono 
381792     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powMono 
381808     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 12.77ms 
381809     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powMonoConcrete.proof 
381809     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 83.7ns 
381810     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
384783     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.97s 
384783     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powMonoConcrete 
385696     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powMonoConcrete 
385700     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.25ms 
385702     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powMonoConcreteRight.proof 
385702     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 62.3ns 
385702     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
388440     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.74s 
388440     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powMonoConcreteRight 
389354     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powMonoConcreteRight 
389357     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 641.01ns 
389358     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powPositive.proof 
389358     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 77.5ns 
389359     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
392089     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.73s 
392089     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powPositive 
392999     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powPositive 
393006     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.32ms 
393007     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powPositiveConcrete.proof 
393007     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 84.8ns 
393008     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
395916     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.91s 
395917     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powPositiveConcrete 
396965     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powPositiveConcrete 
396968     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 780.01ns 
396970     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powGeq1Concrete.proof 
396970     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 71.3ns 
396971     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
399798     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.83s 
399798     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powGeq1Concrete 
400706     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powGeq1Concrete 
400709     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 638.51ns 
400710     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_pow2InIntLower.proof 
400710     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 58ns 
400711     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
403607     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.9s 
403607     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: pow2InIntLower 
404520     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: pow2InIntLower 
404522     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 676.61ns 
404524     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_pow2InIntUpper.proof 
404525     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 229.1ns 
404525     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
407282     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.76s 
407282     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: pow2InIntUpper 
408263     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: pow2InIntUpper 
408268     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.24ms 
408269     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logSelfConcrete.proof 
408269     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 61.5ns 
408270     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
411192     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.92s 
411192     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logSelfConcrete 
412164     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logSelfConcrete 
412180     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 13.54ms 
412183     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_log1Concrete.proof 
412185     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 1.17ms 
412186     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
415088     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.9s 
415088     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: log1Concrete 
415988     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: log1Concrete 
415993     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.62ms 
415994     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logProduct.proof 
415994     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 72.7ns 
415995     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
418692     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.7s 
418692     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logProduct 
419619     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logProduct 
419628     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 6ms 
419629     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logTimesBaseConcrete.proof 
419629     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 63.1ns 
419630     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
422386     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.76s 
422386     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logTimesBaseConcrete 
423280     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logTimesBaseConcrete 
423284     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.64ms 
423286     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logProdIdentity.proof 
423286     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 95.4ns 
423286     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
426008     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.72s 
426008     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logProdIdentity 
426962     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logProdIdentity 
426981     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 15.78ms 
426982     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logProdIdentityConcrete.proof 
426982     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 80.6ns 
426983     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
429871     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.89s 
429872     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logProdIdentityConcrete 
430806     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logProdIdentityConcrete 
430810     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.97ms 
430811     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logPowIdentity.proof 
430811     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 56.8ns 
430812     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
433658     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.85s 
433658     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logPowIdentity 
434616     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logPowIdentity 
434620     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.36ms 
434621     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logPowIdentityConcrete.proof 
434621     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 77ns 
434622     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
437528     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.91s 
437528     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logPowIdentityConcrete 
438486     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logPowIdentityConcrete 
438491     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.52ms 
438493     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logPositive.proof 
438493     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 62.8ns 
438493     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
441385     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.89s 
441385     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logPositive 
442361     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logPositive 
442384     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 19.06ms 
442387     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logPositiveConcrete.proof 
442387     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 232.7ns 
442388     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
445255     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.87s 
445255     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logPositiveConcrete 
446166     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logPositiveConcrete 
446171     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 602.01ns 
446174     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logMono.proof 
446174     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 740.01ns 
446175     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
448872     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.7s 
448872     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logMono 
449769     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logMono 
449815     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 40.97ms 
449816     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logMonoConcrete.proof 
449816     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 92.7ns 
449817     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
452549     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.73s 
452549     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logMonoConcrete 
453430     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logMonoConcrete 
453434     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2ms 
453436     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powLogLess.proof 
453436     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 60.2ns 
453436     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
456371     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.93s 
456372     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powLogLess 
457251     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powLogLess 
457277     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 22.76ms 
457279     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powLogMore2.proof 
457279     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 80.2ns 
457279     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
460162     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.88s 
460162     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powLogMore2 
461152     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powLogMore2 
461182     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 26.11ms 
461183     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logLessThanPow.proof 
461183     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 83.5ns 
461185     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
464213     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.03s 
464213     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logLessThanPow 
465094     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logLessThanPow 
465123     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 24.96ms 
465124     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logLessThanPowConcrete.proof 
465125     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 89.7ns 
465125     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
467895     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.77s 
467895     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logLessThanPowConcrete 
468780     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logLessThanPowConcrete 
468782     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 643.11ns 
468784     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logSqueeze.proof 
468784     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 61.4ns 
468784     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
471619     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.83s 
471620     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logSqueeze 
472500     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logSqueeze 
472506     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.52ms 
472508     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/booleanRules/Taclet_ifthenelse_equals.proof 
472508     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 70.5ns 
472509     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
475328     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.82s 
475329     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: ifthenelse_equals 
476213     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: ifthenelse_equals 
476217     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.46ms 
476218     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/booleanRules/Taclet_ifthenelse_equals_1.proof 
476218     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 72ns 
476219     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
479147     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.93s 
479147     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: ifthenelse_equals_1 
480067     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: ifthenelse_equals_1 
480070     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 873.61ns 
480071     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/booleanRules/Taclet_ifthenelse_equals_2.proof 
480072     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 77.2ns 
480072     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
482847     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.77s 
482847     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: ifthenelse_equals_2 
483800     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: ifthenelse_equals_2 
483803     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.07ms 
483805     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/locSet/Taclet_disjointWithSingleton1.proof 
483805     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 61.3ns 
483805     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
486768     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.96s 
486769     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: disjointWithSingleton1 
487710     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: disjointWithSingleton1 
487751     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.86ms 
487752     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/locSet/Taclet_disjointWithSingleton2.proof 
487752     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 76.9ns 
487753     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
490579     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.83s 
490579     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: disjointWithSingleton2 
491568     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: disjointWithSingleton2 
491574     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.87ms 
491576     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/locSet/Taclet_disjointArrayRanges.proof 
491576     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 78.8ns 
491577     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
494420     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.84s 
494421     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: disjointArrayRanges 
495400     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: disjointArrayRanges 
495412     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 9.28ms 
495413     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/locSet/Taclet_disjointArrayRangeAllFields1.proof 
495413     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 73.1ns 
495414     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
498320     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.91s 
498320     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: disjointArrayRangeAllFields1 
499309     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: disjointArrayRangeAllFields1 
499324     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 13.04ms 
499329     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/locSet/Taclet_disjointArrayRangeAllFields2.proof 
499330     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 262.1ns 
499331     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
502199     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.87s 
502199     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: disjointArrayRangeAllFields2 
503109     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: disjointArrayRangeAllFields2 
503122     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 11.13ms 
503123     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqSelfDefinition.proof 
503124     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 79.6ns 
503124     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
505807     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.68s 
505807     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqSelfDefinition 
506714     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqSelfDefinition 
506734     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 16.99ms 
506735     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqOutsideValue.proof 
506735     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 99ns 
506736     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
509469     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.73s 
509469     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqOutsideValue 
510405     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqOutsideValue 
510411     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.9ms 
510413     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_castedGetAny.proof 
510414     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 234.3ns 
510415     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
513104     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.69s 
513104     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: castedGetAny 
514027     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: castedGetAny 
514033     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.7ms 
514034     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqGetAlphaCast.proof 
514034     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 63.5ns 
514035     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
516829     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.79s 
516829     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqGetAlphaCast 
517818     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqGetAlphaCast 
517821     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 744.51ns 
517822     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqSingleton.proof 
517822     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 75.2ns 
517823     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
520738     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.92s 
520738     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqSingleton 
521632     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqSingleton 
521636     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.57ms 
521637     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqSingletonConcrete.proof 
521637     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 71.6ns 
521638     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
524360     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.72s 
524360     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqSingletonConcrete 
525245     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqSingletonConcrete 
525248     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.02ms 
525249     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqConcat.proof 
525249     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 67.5ns 
525250     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
528091     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.84s 
528091     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqConcat 
528997     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqConcat 
529010     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 10.21ms 
529011     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqSub.proof 
529011     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 72.2ns 
529012     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
531730     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.72s 
531731     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqSub 
532645     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqSub 
532649     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.81ms 
532651     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqReverse.proof 
532651     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 76.3ns 
532651     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
535357     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.71s 
535358     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqReverse 
536283     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqReverse 
536291     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 5.67ms 
536292     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqEmpty.proof 
536292     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 65.2ns 
536293     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
539004     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.71s 
539004     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqEmpty 
539923     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqEmpty 
539926     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 834.61ns 
539927     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqSingleton.proof 
539927     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 68.5ns 
539928     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
542703     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.78s 
542703     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqSingleton 
543678     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqSingleton 
543680     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 702.51ns 
543682     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqConcat.proof 
543682     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 67.5ns 
543682     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
546521     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.84s 
546521     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqConcat 
547474     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqConcat 
547479     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.58ms 
547480     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqSub.proof 
547482     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 122.6ns 
547483     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
550422     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.94s 
550422     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqSub 
551374     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqSub 
551378     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2ms 
551380     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqReverse.proof 
551380     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 68.2ns 
551380     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
554250     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.87s 
554250     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqReverse 
555175     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqReverse 
555179     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.67ms 
555180     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_equalityToSeqGetAndSeqLenLeft.proof 
555180     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 57.4ns 
555181     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
557875     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.69s 
557876     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: equalityToSeqGetAndSeqLenLeft 
558781     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: equalityToSeqGetAndSeqLenLeft 
558784     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.47ms 
558785     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_equalityToSeqGetAndSeqLenRight.proof 
558785     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 75ns 
558786     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
561556     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.77s 
561557     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: equalityToSeqGetAndSeqLenRight 
562542     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: equalityToSeqGetAndSeqLenRight 
562548     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.42ms 
562549     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqSingletonEQ.proof 
562549     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 70.1ns 
562550     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
565407     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.86s 
565407     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqSingletonEQ 
566385     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqSingletonEQ 
566389     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.24ms 
566390     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqConcatEQ.proof 
566390     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 72ns 
566391     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
569321     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.93s 
569321     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqConcatEQ 
570203     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqConcatEQ 
570216     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 10.7ms 
570217     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqSubEQ.proof 
570217     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 65.2ns 
570218     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
573144     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.93s 
573145     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqSubEQ 
574069     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqSubEQ 
574071     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 734.41ns 
574072     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqReverseEQ.proof 
574073     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 68.9ns 
574073     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
576992     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.92s 
576992     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqReverseEQ 
577983     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqReverseEQ 
577993     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 7.61ms 
577995     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqEmptyEQ.proof 
577995     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 78.5ns 
577996     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
580883     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.89s 
580884     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqEmptyEQ 
581867     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqEmptyEQ 
581871     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.07ms 
581872     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqSingletonEQ.proof 
581872     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 55.7ns 
581873     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
584995     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.12s 
584996     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqSingletonEQ 
585939     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqSingletonEQ 
585941     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 895.91ns 
585943     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqConcatEQ.proof 
585943     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 58.1ns 
585944     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
588705     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.76s 
588706     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqConcatEQ 
589660     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqConcatEQ 
589670     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 7.93ms 
589672     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqSubEQ.proof 
589672     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 97.8ns 
589673     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
592432     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.76s 
592432     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqSubEQ 
593350     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqSubEQ 
593353     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.85ms 
593355     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqReverseEQ.proof 
593355     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 71.3ns 
593356     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
596212     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.86s 
596212     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqReverseEQ 
597108     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqReverseEQ 
597113     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.6ms 
597116     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqDefEQ.proof 
597116     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 405.4ns 
597117     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
600086     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.97s 
600086     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqDefEQ 
601105     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqDefEQ 
601110     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.51ms 
601111     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqDefEQ.proof 
601111     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 72.2ns 
601112     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
603928     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.82s 
603928     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqDefEQ 
604861     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqDefEQ 
604871     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 7.09ms 
604873     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqConcatWithSeqEmpty1.proof 
604873     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 77.3ns 
604873     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
607778     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.9s 
607779     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqConcatWithSeqEmpty1 
608760     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqConcatWithSeqEmpty1 
608779     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 15.5ms 
608781     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqConcatWithSeqEmpty2.proof 
608781     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 222.6ns 
608782     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
611518     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.74s 
611518     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqConcatWithSeqEmpty2 
612434     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqConcatWithSeqEmpty2 
612452     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 16.21ms 
612453     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqReverseOfSeqEmpty.proof 
612453     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 81ns 
612454     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
615140     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.69s 
615140     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqReverseOfSeqEmpty 
616046     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqReverseOfSeqEmpty 
616058     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 10.33ms 
616059     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_subSeqComplete.proof 
616060     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 69.7ns 
616060     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
618743     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.68s 
618743     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: subSeqComplete 
619667     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: subSeqComplete 
619680     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 10.92ms 
619682     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_subSeqTailR.proof 
619682     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 75.1ns 
619682     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
622559     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.88s 
622559     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: subSeqTailR 
623550     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: subSeqTailR 
623583     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 30.01ms 
623584     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_subSeqTailL.proof 
623584     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 59.1ns 
623585     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
626439     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.85s 
626439     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: subSeqTailL 
627368     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: subSeqTailL 
627399     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 28.38ms 
627401     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_subSeqTailEQR.proof 
627401     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 82.8ns 
627402     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
630175     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.77s 
630175     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: subSeqTailEQR 
631065     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: subSeqTailEQR 
631093     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 26.17ms 
631095     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_subSeqTailEQL.proof 
631095     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 65.1ns 
631096     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
633979     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.88s 
633979     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: subSeqTailEQL 
634966     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: subSeqTailEQL 
634984     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 14.94ms 
634986     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDef_split.proof 
634986     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 85.5ns 
634986     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
637898     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.91s 
637898     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_split 
638839     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDef_split 
638878     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 35.14ms 
638879     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDef_induction_upper.proof 
638879     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 68.9ns 
638880     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
641635     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.75s 
641635     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_induction_upper 
642635     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDef_induction_upper 
642698     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 58.59ms 
642699     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDef_induction_upper_concrete.proof 
642700     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 77.1ns 
642700     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
645617     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.92s 
645617     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_induction_upper_concrete 
646633     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDef_induction_upper_concrete 
646687     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 48.99ms 
646695     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDef_induction_lower.proof 
646696     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 260.8ns 
646697     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
649688     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.99s 
649689     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_induction_lower 
650687     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDef_induction_lower 
650740     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 50.06ms 
650742     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDef_induction_lower_concrete.proof 
650742     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 246.4ns 
650743     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
653644     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.9s 
653644     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_induction_lower_concrete 
654680     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDef_induction_lower_concrete 
654748     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 63.07ms 
654749     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDef_split_in_three.proof 
654750     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 242.3ns 
654751     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
657579     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.83s 
657579     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_split_in_three 
658547     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDef_split_in_three 
658694     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 138.97ms 
658695     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDef_empty.proof 
658696     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 68ns 
658696     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
661440     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.74s 
661440     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_empty 
662374     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDef_empty 
662384     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 7.22ms 
662385     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDef_one_summand.proof 
662385     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 60.8ns 
662386     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
665135     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.75s 
665135     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_one_summand 
666062     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDef_one_summand 
666073     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 7.61ms 
666074     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDef_lower_equals_upper.proof 
666074     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 77ns 
666075     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
668952     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.88s 
668953     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_lower_equals_upper 
669877     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDef_lower_equals_upper 
669883     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.39ms 
669884     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDefOfSeq.proof 
669884     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 80.4ns 
669885     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
672761     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.88s 
672762     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDefOfSeq 
673771     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDefOfSeq 
673800     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 24.92ms 
673801     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqSelfDefinitionEQ2.proof 
673801     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 78.5ns 
673802     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
676754     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.95s 
676754     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqSelfDefinitionEQ2 
677759     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqSelfDefinitionEQ2 
677774     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 12.03ms 
677776     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_indexOfSeqSingleton.proof 
677776     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 83.8ns 
677776     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
680674     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.9s 
680674     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: indexOfSeqSingleton 
681614     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: indexOfSeqSingleton 
681617     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.05ms 
681619     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_indexOfSeqConcatFirst.proof 
681619     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 76.5ns 
681620     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
684407     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.79s 
684407     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: indexOfSeqConcatFirst 
685414     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: indexOfSeqConcatFirst 
685436     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 19.36ms 
685437     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_indexOfSeqConcatSecond.proof 
685437     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 65.2ns 
685438     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
688348     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.91s 
688348     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: indexOfSeqConcatSecond 
689304     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: indexOfSeqConcatSecond 
689325     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 18.59ms 
689327     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_indexOfSeqSub.proof 
689327     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 75.6ns 
689328     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
692257     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.93s 
692257     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: indexOfSeqSub 
693233     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: indexOfSeqSub 
693257     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 20.38ms 
693258     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfArray2seq.proof 
693258     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 77.2ns 
693259     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
696260     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3s 
696261     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfArray2seq 
697185     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfArray2seq 
697188     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.42ms 
697189     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getAnyOfArray2seq.proof 
697190     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 68.9ns 
697190     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
699936     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.75s 
699936     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getAnyOfArray2seq 
700838     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getAnyOfArray2seq 
700842     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.35ms 
700844     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfArray2seq.proof 
700844     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 73.7ns 
700844     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
703592     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.75s 
703592     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfArray2seq 
704516     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfArray2seq 
704524     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 5.41ms 
704525     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_getAnyOfNPermInv.proof 
704525     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 75ns 
704526     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
707441     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.92s 
707441     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getAnyOfNPermInv 
708441     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getAnyOfNPermInv 
708449     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 5.37ms 
708450     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqNPermRange.proof 
708450     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 78ns 
708451     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
711327     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.88s 
711327     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqNPermRange 
712258     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqNPermRange 
712343     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 77.45ms 
712345     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermTrans.proof 
712345     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 89.3ns 
712346     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
715293     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.95s 
715293     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermTrans 
716277     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermTrans 
716322     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 41.18ms 
716324     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermRefl.proof 
716324     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 84.9ns 
716325     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
719270     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.94s 
719270     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermRefl 
720296     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermRefl 
720361     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 62.31ms 
720363     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermSplit.proof 
720363     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 81.8ns 
720364     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
723319     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.95s 
723319     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermSplit 
724305     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermSplit 
724307     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 404.8ns 
724309     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqNPermRight.proof 
724310     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 201.2ns 
724311     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
727239     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.93s 
727239     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqNPermRight 
728243     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqNPermRight 
728508     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 251.89ms 
728511     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermFromSwap.proof 
728512     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 241.9ns 
728513     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
731474     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.96s 
731474     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermFromSwap 
732467     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermFromSwap 
732533     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 60.09ms 
732535     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermTransAlt0.proof 
732535     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 65.2ns 
732535     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
735411     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.88s 
735411     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermTransAlt0 
736387     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermTransAlt0 
736389     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 375.2ns 
736391     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermTransAlt1.proof 
736391     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 70.7ns 
736393     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
739283     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.89s 
739283     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermTransAlt1 
740259     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermTransAlt1 
740261     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 386.6ns 
740262     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermTransAlt2.proof 
740262     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 71.3ns 
740263     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
743176     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.91s 
743176     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermTransAlt2 
744156     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermTransAlt2 
744158     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 504.61ns 
744160     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermTransAlt3.proof 
744160     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 130.6ns 
744161     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
746995     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.83s 
746995     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermTransAlt3 
747976     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermTransAlt3 
747979     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 583.71ns 
747980     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermForall.proof 
747981     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 67.4ns 
747981     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
750827     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.85s 
750827     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermForall 
751793     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermForall 
751891     INFO  Test worker     d.u.i.k.s.SMTFocusResults Analyzing unsat core: (L_1 L_3 L_4) 
751908     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 112.7ms 
751911     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermExists.proof 
751912     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 243.1ns 
751913     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
754866     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.95s 
754866     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermExists 
755823     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermExists 
755888     INFO  Test worker     d.u.i.k.s.SMTFocusResults Analyzing unsat core: (L_1 L_3 L_5 L_6 L_7) 
755890     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 63.73ms 
755892     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm2/Taclet_schiffl_lemma_2.proof 
755892     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 68.4ns 
755894     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
758813     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.92s 
758814     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: schiffl_lemma_2 
759807     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: schiffl_lemma_2 
759809     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.3ns 
759842     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 1: 'macro split-prop' 
759900     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 2: 'rule allRight' 
759922     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 3: 'rule allRight' 
759926     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 4: 'macro split-prop' 
759932     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 5: 'rule 'seqPermDefLeft'' 
759935     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 6: 'rule 'andLeft'' 
759936     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 7: 'rule 'exLeft'' 
759938     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 8: 'macro split-prop' 
759941     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 9: 'rule  seqNPermRange' 
759943     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 10: 'instantiate var=iv with='v_x_0' occ=1' 
759946     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 11: 'rule impLeft' 
759947     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 12: 'tryclose branch' 
760124     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 13: 'rule andLeft' 
760125     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 14: 'rule andLeft' 
760126     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 15: 'instantiate var=iv with='v_y_0' occ=1' 
760128     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 16: 'rule impLeft' 
760129     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 17: 'tryclose branch' 
760245     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 18: 'rule andLeft' 
760246     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 19: 'rule andLeft' 
760247     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 20: 'rule seqNPermDefLeft' 
760249     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 21: 'instantiate var=iv with='v_x_0' occ=2' 
760251     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 22: 'rule impLeft' 
760252     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 23: 'tryclose branch' 
760432     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 24: 'rule exLeft' 
760434     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 25: 'rule andLeft' 
760436     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 26: 'rule andLeft' 
760438     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 27: 'instantiate hide var=iv with='v_y_0' occ=2' 
760440     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 28: 'rule impLeft' 
760444     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 29: 'tryclose branch' 
760592     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 30: 'rule exLeft' 
760594     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 31: 'rule andLeft' 
760596     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 32: 'rule andLeft' 
760597     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 33: 'instantiate var=iv with='jv_0' occ=1' 
760598     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 34: 'rule impLeft' 
760599     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 35: 'tryclose branch' 
760608     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 36: 'rule andLeft' 
760609     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 37: 'rule andLeft' 
760610     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 38: 'rule castAdd formula='s_0[jv_0] = v_x_0' occ=0' 
760612     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 39: 'instantiate hide var=iv with='jv_1' occ=1' 
760615     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 40: 'rule impLeft' 
760616     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 41: 'tryclose branch' 
760626     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 42: 'rule andLeft' 
760627     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 43: 'rule andLeft' 
760628     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 44: 'rule castAdd formula='s_0[jv_1] = v_y_0' occ=0' 
760629     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 45: 'instantiate var=iv  with='v_x_0'' 
760630     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 46: 'rule impLeft' 
760631     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 47: 'tryclose branch' 
760806     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 48: 'instantiate var=iv  with='v_y_0'' 
760807     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 49: 'rule impLeft' 
760809     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 50: 'tryclose branch' 
761000     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 51: 'cut 'v_x_0 = v_y_0'' 
761002     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)'' 
761005     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 53: 'rule andRight' 
761006     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 54: 'rule andRight' 
761007     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 55: 'rule andRight' 
761009     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 56: 'rule andRight' 
761010     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 57: 'rule lenOfSwap' 
761013     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 58: 'tryclose branch' 
761017     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 59: 'rule seqNPermSwapNPerm' 
761020     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 60: 'instantiate hide var='iv' with='v_x_0' occ=1' 
761021     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 61: 'instantiate hide var='jv' with='jv_0'' 
761022     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 62: 'rule impLeft' 
761023     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 63: 'tryclose branch' 
761151     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 64: 'tryclose branch' 
761155     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 65: 'rule allRight' 
761157     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 66: 'rule impRight' 
761158     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 67: 'rule andLeft' 
761159     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 68: 'instantiate var=iv with='v_iv_0'' 
761160     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 69: 'rule impLeft' 
761162     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 70: 'tryclose branch' 
761297     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 71: 'rule getOfSwap' 
761299     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 72: 'rule ifthenelse_negated' 
761300     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 73: 'rule ifthenelse_split occ=0' 
761302     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 74: 'rule andLeft' 
761303     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 75: 'rule andLeft' 
761304     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 76: 'rule andLeft' 
761306     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 77: 'rule ifthenelse_split occ=0' 
761307     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 78: 'tryclose branch' 
761413     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 79: 'rule ifthenelse_split occ=0' 
761415     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 80: 'tryclose branch' 
761514     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 81: 'tryclose branch' 
761518     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 82: 'tryclose branch' 
761531     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 83: 'rule getOfSwap' 
761532     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 84: 'rule ifthenelse_negated' 
761535     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 85: 'rule ifthenelse_split occ=0' 
761537     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 86: 'rule andLeft' 
761538     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 87: 'rule andLeft' 
761539     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 88: 'rule andLeft' 
761539     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 89: 'rule ifthenelse_split occ=0' 
761541     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 90: 'tryclose branch' 
761551     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 91: 'tryclose branch' 
761556     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 92: 'tryclose branch' 
761663     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 93: 'rule getOfSwap' 
761665     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 94: 'rule ifthenelse_negated' 
761667     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 95: 'rule ifthenelse_split occ=0' 
761669     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 96: 'rule andLeft' 
761669     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 97: 'rule andLeft' 
761670     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 98: 'rule andLeft' 
761670     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 99: 'rule ifthenelse_split occ=0' 
761672     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 100: 'tryclose branch' 
761731     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 101: 'tryclose branch' 
761736     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 102: 'tryclose branch' 
761845     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 103: 'cut '(int)s_0[v_x_0] = (int)s_0[v_y_0]'' 
761847     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 104: 'rule seqNPermInjective' 
761850     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 105: 'instantiate hide var=iv with='v_x_0'' 
761852     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 106: 'instantiate hide var=jv with='v_y_0'' 
761853     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 107: 'rule impLeft' 
761854     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 108: 'tryclose branch' 
762016     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 109: 'tryclose branch' 
762021     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 110: 'cut '(int)s_0[v_x_0] = v_x_0'' 
762025     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)'' 
762027     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 112: 'rule andRight' 
762029     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 113: 'rule andRight' 
762030     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 114: 'rule andRight' 
762031     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 115: 'rule andRight' 
762032     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 116: 'tryclose branch' 
762042     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 117: 'rule seqNPermSwapNPerm' 
762049     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 118: 'instantiate hide var=iv with='v_y_0'' 
762051     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 119: 'instantiate hide var=jv with='jv_1'' 
762053     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 120: 'tryclose branch' 
762178     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 121: 'rule allRight' 
762180     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 122: 'rule impRight' 
762181     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 123: 'rule andLeft' 
762183     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 124: 'instantiate var=iv with='v_iv_0'' 
762184     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 125: 'rule impLeft' 
762185     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 126: 'tryclose branch' 
762312     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 127: 'rule getOfSwap' 
762314     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 128: 'rule ifthenelse_negated' 
762321     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 129: 'rule ifthenelse_split occ=0' 
762323     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 130: 'rule andLeft' 
762324     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 131: 'rule andLeft' 
762325     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 132: 'rule andLeft' 
762326     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 133: 'rule ifthenelse_split occ=0' 
762327     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 134: 'tryclose branch' 
762419     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 135: 'rule ifthenelse_split occ=0' 
762421     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 136: 'tryclose branch' 
762507     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 137: 'instantiate var=iv with='v_y_0'' 
762508     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 138: 'rule impLeft' 
762509     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 139: 'tryclose branch' 
762514     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 140: 'tryclose branch' 
762518     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 141: 'tryclose branch' 
762523     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 142: 'tryclose branch' 
762710     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 143: 'rule getOfSwap' 
762712     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 144: 'rule ifthenelse_negated' 
762713     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 145: 'rule ifthenelse_split occ=0' 
762714     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 146: 'tryclose branch' 
762726     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 147: 'tryclose branch' 
762834     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 148: 'tryclose branch' 
767034     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 149: 'cut  '(int)s_0[v_y_0] = v_y_0'' 
767035     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)'' 
767043     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 151: 'rule andRight' 
767044     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 152: 'rule andRight' 
767045     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 153: 'rule andRight' 
767046     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 154: 'rule andRight' 
767047     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 155: 'tryclose branch' 
767056     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 156: 'rule seqNPermSwapNPerm' 
767058     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 157: 'instantiate hide var=iv with='v_x_0'' 
767059     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 158: 'instantiate hide var=jv with='jv_0'' 
767060     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 159: 'rule impLeft' 
767062     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 160: 'tryclose branch' 
767177     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 161: 'tryclose branch' 
767183     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 162: 'rule allRight' 
767185     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 163: 'rule impRight' 
767186     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 164: 'rule andLeft' 
767186     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 165: 'instantiate var=iv with='v_iv_0'' 
767187     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 166: 'rule impLeft' 
767188     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 167: 'tryclose branch' 
767312     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 168: 'rule getOfSwap' 
767313     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 169: 'rule ifthenelse_negated' 
767314     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 170: 'rule ifthenelse_split occ=0' 
767316     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 171: 'rule andLeft' 
767316     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 172: 'rule andLeft' 
767317     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 173: 'rule andLeft' 
767318     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 174: 'rule ifthenelse_split occ=0' 
767320     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 175: 'tryclose branch' 
767421     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 176: 'rule ifthenelse_split occ=0' 
767423     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 177: 'tryclose branch' 
767521     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 178: 'tryclose branch' 
767526     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 179: 'tryclose branch' 
767531     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 180: 'rule getOfSwap' 
767532     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 181: 'rule ifthenelse_negated' 
767533     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 182: 'rule ifthenelse_split occ=0' 
767534     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 183: 'tryclose branch' 
767546     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 184: 'tryclose branch' 
767649     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 185: 'rule getOfSwap' 
767650     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 186: 'rule ifthenelse_negated' 
767651     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 187: 'rule ifthenelse_split occ=0' 
767653     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 188: 'tryclose branch' 
767748     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 189: 'tryclose branch' 
767759     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 190: 'cut '(int)s_0[v_x_0]=v_y_0'' 
767760     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)'' 
767762     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 192: 'rule andRight' 
767763     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 193: 'rule andRight' 
767763     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 194: 'rule andRight' 
767764     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 195: 'rule andRight' 
767765     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 196: 'tryclose branch' 
767779     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 197: 'rule seqNPermSwapNPerm' 
767780     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 198: 'instantiate hide var=iv with='jv_0'' 
767781     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 199: 'instantiate hide var=jv with='v_x_0'' 
767782     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 200: 'rule impLeft' 
767782     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 201: 'tryclose branch' 
767889     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 202: 'rule seqNPermSwapNPerm formula='seqNPerm(seqSwap(s_0, jv_0, v_x_0))'' 
767891     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 203: 'instantiate hide var=iv with='jv_0'' 
767893     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 204: 'instantiate hide var=jv with='v_y_0'' 
767895     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 205: 'rule impLeft' 
767896     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 206: 'tryclose branch' 
768002     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 207: 'tryclose branch' 
768007     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 208: 'rule allRight' 
768009     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 209: 'rule impRight' 
768009     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 210: 'rule andLeft' 
768010     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 211: 'instantiate var=iv with='v_iv_0'' 
768011     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 212: 'rule impLeft' 
768012     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 213: 'tryclose branch' 
768125     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 214: 'rule getOfSwap' 
768127     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 215: 'rule ifthenelse_negated' 
768128     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 216: 'rule ifthenelse_split occ=0' 
768129     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 217: 'rule andLeft' 
768130     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 218: 'rule andLeft' 
768130     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 219: 'rule andLeft' 
768131     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 220: 'rule ifthenelse_split occ=0' 
768132     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 221: 'rule getOfSwap' 
768133     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 222: 'rule ifthenelse_negated' 
768134     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 223: 'rule ifthenelse_split occ=0' 
768139     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 224: 'rule andLeft' 
768140     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 225: 'rule andLeft' 
768140     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 226: 'rule andLeft' 
768141     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 227: 'rule ifthenelse_split occ=0' 
768142     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 228: 'tryclose branch' 
768312     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 229: 'rule ifthenelse_split occ=0' 
768313     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 230: 'tryclose branch' 
768321     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 231: 'tryclose branch' 
768414     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 232: 'tryclose branch' 
768506     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 233: 'rule ifthenelse_split' 
768508     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 234: 'rule getOfSwap' 
768509     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 235: 'rule ifthenelse_negated' 
768510     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 236: 'rule ifthenelse_split occ=0' 
768511     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 237: 'rule andLeft' 
768512     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 238: 'rule andLeft' 
768512     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 239: 'rule andLeft' 
768513     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 240: 'rule ifthenelse_split occ=0' 
768514     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 241: 'tryclose branch' 
768617     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 242: 'tryclose branch' 
768625     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 243: 'tryclose branch' 
768728     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 244: 'rule getOfSwap' 
768730     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 245: 'rule ifthenelse_negated' 
768731     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 246: 'rule ifthenelse_split occ=0' 
768732     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 247: 'rule andLeft' 
768732     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 248: 'rule andLeft' 
768733     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 249: 'rule andLeft' 
768733     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 250: 'rule ifthenelse_split occ=0' 
768734     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 251: 'tryclose branch' 
768740     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 252: 'rule ifthenelse_split occ=0' 
768741     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 253: 'tryclose branch' 
768832     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 254: 'tryclose branch' 
768837     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 255: 'tryclose branch' 
768844     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 256: 'tryclose branch' 
768957     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 257: 'rule getOfSwap' 
768958     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 258: 'rule ifthenelse_negated' 
768959     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 259: 'rule ifthenelse_split occ=0' 
768960     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 260: 'rule andLeft' 
768961     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 261: 'rule andLeft' 
768961     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 262: 'rule andLeft' 
768962     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 263: 'rule ifthenelse_split occ=0' 
768963     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 264: 'tryclose branch' 
769025     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 265: 'rule ifthenelse_split occ=0' 
769026     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 266: 'rule getOfSwap' 
769027     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 267: 'rule ifthenelse_negated' 
769028     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 268: 'rule ifthenelse_split occ=0' 
769029     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 269: 'tryclose branch' 
769036     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 270: 'tryclose branch' 
769042     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 271: 'tryclose branch' 
769175     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 272: 'tryclose branch' 
769277     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 273: 'rule getOfSwap' 
769278     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 274: 'rule ifthenelse_negated' 
769279     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 275: 'rule ifthenelse_split occ=0' 
769280     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 276: 'tryclose branch' 
769472     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 277: 'tryclose branch' 
769574     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 278: 'cut 'int::seqGet(s_0, v_y_0)=v_x_0'' 
769575     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 279: 'tryclose branch' 
773151     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 280: 'rule seqNPermSwapNPerm' 
773157     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 281: 'instantiate hide var=iv with='jv_1'' 
773159     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 282: 'instantiate hide var=jv with='v_y_0'' 
773160     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 283: 'rule impLeft' 
773161     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 284: 'tryclose branch' 
773308     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 285: 'rule seqNPermSwapNPerm formula='seqNPerm(seqSwap(s_0,jv_1,v_y_0))'' 
773310     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 286: 'instantiate hide var=iv with='jv_1'' 
773312     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 287: 'instantiate hide var=jv with='v_x_0'' 
773313     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 288: 'rule impLeft' 
773314     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 289: 'tryclose branch' 
773466     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 290: 'tryclose branch' 
777194     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 291: 'tryclose branch' 
781541     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 292: 'rule seqNPermSwapNPerm formula='seqNPerm(s_0)'' 
781547     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 293: 'instantiate hide var=iv with='v_x_0'' 
781549     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 294: 'instantiate hide var=jv with='jv_0'' 
781550     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 295: 'rule impLeft' 
781550     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 296: 'tryclose branch' 
781682     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 297: 'rule seqNPermSwapNPerm formula='seqNPerm(seqSwap(s_0,v_x_0,jv_0))'' 
781683     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 298: 'instantiate hide var=iv with='v_y_0'' 
781684     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 299: 'instantiate hide var=jv with='jv_1'' 
781685     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)' ...' 
781687     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 301: 'tryclose branch' 
783008     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm2/Taclet_schiffl_thm_1.proof 
783008     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 104ns 
783009     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
785865     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.86s 
785865     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: schiffl_thm_1 
786868     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: schiffl_thm_1 
786869     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 8.4ns 
786870     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 1: 'macro split-prop' 
786884     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 2: 'rule schiffl_lemma_2 formula='seqPerm(f_s, f_t)'' 
786904     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 3: 'instantiate hide var=x with='f_x'' 
786907     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 4: 'instantiate hide var=y with='f_y'' 
786913     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 5: 'rule impLeft' 
786913     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 6: 'tryclose branch' 
786919     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 7: 'rule exLeft' 
786921     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 8: 'macro split-prop' 
786925     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 9: 'rule seqPermDef occ=1' 
786929     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 10: 'rule andRight' 
786929     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 11: 'tryclose branch' 
786940     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 12: 'instantiate hide var=s with='r_0'' 
786943     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 13: 'rule andRight' 
786943     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 14: 'tryclose branch' 
787001     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 15: 'rule allRight' 
787002     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 16: 'rule impRight' 
787003     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 17: 'instantiate hide var=iv with='iv_0'' 
787004     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 18: 'rule impLeft' 
787004     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 19: 'tryclose branch' 
787083     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 20: 'rule andLeft' 
787084     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 21: 'rule seqNPermRange' 
787085     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 22: 'instantiate hide var=iv with='iv_0'' 
787086     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 23: 'rule impLeft' 
787087     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 24: 'tryclose branch' 
787091     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 25: 'rule andLeft' 
787092     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 26: 'rule andLeft' 
787093     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 27: 'rule seqNPermRange' 
787094     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 28: 'instantiate hide var=iv with='f_x'' 
787095     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 29: 'rule impLeft' 
787096     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 30: 'tryclose branch' 
787192     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 31: 'rule andLeft' 
787193     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 32: 'rule andLeft' 
787194     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 33: 'rule seqNPermRange' 
787196     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 34: 'instantiate hide var=iv with='f_y'' 
787197     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 35: 'rule impLeft' 
787198     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 36: 'tryclose branch' 
787305     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 37: 'rule andLeft' 
787306     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 38: 'rule andLeft' 
787307     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 39: 'rule getOfSeqDef occ=0' 
787307     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 40: 'rule getOfSeqDef' 
787308     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 41: 'rule ifthenelse_split occ=0' 
787309     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 42: 'rule andLeft occ=0' 
787310     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 43: 'rule sub_zero_2 occ=0' 
787311     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 44: 'rule ifthenelse_split occ=2' 
787312     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 45: 'rule andLeft' 
787312     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 46: 'rule sub_zero_2 occ=0' 
787313     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 47: 'rule add_zero_right occ=0' 
787314     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 48: 'rule add_zero_right occ=0' 
787314     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 49: 'rule add_zero_right occ=0' 
787315     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 50: 'rule add_zero_right occ=0' 
787316     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 51: 'rule add_zero_right occ=0' 
787316     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 52: 'rule add_zero_right occ=0' 
787317     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 53: 'rule ifthenelse_split occ=0' 
787318     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 54: 'rule ifthenelse_split occ=0' 
787320     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 55: 'tryclose branch' 
787322     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 56: 'tryclose branch' 
787369     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 57: 'rule ifthenelse_split occ=0' 
787371     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 58: 'tryclose branch' 
787445     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 59: 'rule ifthenelse_split occ=0' 
787446     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 60: 'rule seqNPermInjective' 
787448     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 61: 'instantiate hide var=iv with='iv_0'' 
787450     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 62: 'instantiate hide var=jv with='f_y'' 
787451     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 63: 'rule impLeft' 
787452     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 64: 'tryclose branch' 
787522     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 65: 'tryclose branch' 
787528     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 66: 'rule ifthenelse_split occ=0' 
787530     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 67: 'rule seqNPermInjective' 
787532     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 68: 'instantiate hide var=iv with='iv_0'' 
787533     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 69: 'instantiate hide var=jv with='f_x'' 
787535     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 70: 'rule impLeft' 
787536     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 71: 'tryclose branch' 
787605     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 72: 'tryclose branch' 
787609     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 73: 'tryclose branch' 
787612     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 74: 'tryclose branch' 
787697     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 75: 'tryclose branch' 
787774     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_eqSameSeq.proof 
787774     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 271.1ns 
787775     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
790767     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.99s 
790768     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: eqSameSeq 
791726     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: eqSameSeq 
791764     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 34.12ms