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

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

tests
0

failures
0

ignored
12m20.69s

duration
100%

successful

Tests

Test Method name Duration Result
powPositive data()[100] 3.554s passed
powPositiveConcrete data()[101] 3.621s passed
powGeq1Concrete data()[102] 3.549s passed
pow2InIntLower data()[103] 3.595s passed
pow2InIntUpper data()[104] 3.626s passed
logSelfConcrete data()[105] 3.610s passed
log1Concrete data()[106] 3.712s passed
logProduct data()[107] 3.743s passed
logTimesBaseConcrete data()[108] 3.625s passed
logProdIdentity data()[109] 3.665s passed
moduloByteIsInByte data()[10] 3.585s passed
logProdIdentityConcrete data()[110] 3.630s passed
logPowIdentity data()[111] 3.737s passed
logPowIdentityConcrete data()[112] 3.693s passed
logPositive data()[113] 3.666s passed
logPositiveConcrete data()[114] 3.654s passed
logMono data()[115] 3.677s passed
logMonoConcrete data()[116] 3.651s passed
powLogLess data()[117] 3.738s passed
powLogMore2 data()[118] 3.665s passed
logLessThanPow data()[119] 3.662s passed
moduloCharIsInChar data()[11] 3.631s passed
logLessThanPowConcrete data()[120] 3.679s passed
logSqueeze data()[121] 3.629s passed
ifthenelse_equals data()[122] 3.486s passed
ifthenelse_equals_1 data()[123] 3.517s passed
ifthenelse_equals_2 data()[124] 3.451s passed
disjointWithSingleton1 data()[125] 3.453s passed
disjointWithSingleton2 data()[126] 3.615s passed
disjointArrayRanges data()[127] 3.684s passed
disjointArrayRangeAllFields1 data()[128] 3.479s passed
disjointArrayRangeAllFields2 data()[129] 3.436s passed
div_unique1 data()[12] 3.901s passed
seqSelfDefinition data()[130] 3.626s passed
seqOutsideValue data()[131] 3.591s passed
castedGetAny data()[132] 3.545s passed
seqGetAlphaCast data()[133] 3.656s passed
getOfSeqSingleton data()[134] 3.670s passed
getOfSeqSingletonConcrete data()[135] 3.650s passed
getOfSeqConcat data()[136] 3.686s passed
getOfSeqSub data()[137] 3.745s passed
getOfSeqReverse data()[138] 3.602s passed
lenOfSeqEmpty data()[139] 3.614s passed
div_unique2 data()[13] 3.794s passed
lenOfSeqSingleton data()[140] 3.557s passed
lenOfSeqConcat data()[141] 3.470s passed
lenOfSeqSub data()[142] 3.393s passed
lenOfSeqReverse data()[143] 3.423s passed
equalityToSeqGetAndSeqLenLeft data()[144] 3.472s passed
equalityToSeqGetAndSeqLenRight data()[145] 3.539s passed
getOfSeqSingletonEQ data()[146] 3.665s passed
getOfSeqConcatEQ data()[147] 3.565s passed
getOfSeqSubEQ data()[148] 3.477s passed
getOfSeqReverseEQ data()[149] 3.509s passed
div_exists data()[14] 3.799s passed
lenOfSeqEmptyEQ data()[150] 3.492s passed
lenOfSeqSingletonEQ data()[151] 3.415s passed
lenOfSeqConcatEQ data()[152] 3.506s passed
lenOfSeqSubEQ data()[153] 3.409s passed
lenOfSeqReverseEQ data()[154] 3.503s passed
getOfSeqDefEQ data()[155] 3.469s passed
lenOfSeqDefEQ data()[156] 3.485s passed
seqConcatWithSeqEmpty1 data()[157] 3.432s passed
seqConcatWithSeqEmpty2 data()[158] 3.472s passed
seqReverseOfSeqEmpty data()[159] 3.436s passed
div_one data()[15] 3.644s passed
subSeqComplete data()[160] 3.448s passed
subSeqTailR data()[161] 3.624s passed
subSeqTailL data()[162] 3.753s passed
subSeqTailEQR data()[163] 3.588s passed
subSeqTailEQL data()[164] 3.596s passed
seqDef_split data()[165] 3.797s passed
seqDef_induction_upper data()[166] 3.849s passed
seqDef_induction_upper_concrete data()[167] 3.753s passed
seqDef_induction_lower data()[168] 3.665s passed
seqDef_induction_lower_concrete data()[169] 3.635s passed
jdiv_one data()[16] 3.604s passed
seqDef_split_in_three data()[170] 3.649s passed
seqDef_empty data()[171] 3.615s passed
seqDef_one_summand data()[172] 3.615s passed
seqDef_lower_equals_upper data()[173] 3.615s passed
seqDefOfSeq data()[174] 3.936s passed
seqSelfDefinitionEQ2 data()[175] 3.561s passed
indexOfSeqSingleton data()[176] 3.518s passed
indexOfSeqConcatFirst data()[177] 3.515s passed
indexOfSeqConcatSecond data()[178] 3.567s passed
indexOfSeqSub data()[179] 3.534s passed
div_zero data()[17] 3.663s passed
lenOfArray2seq data()[180] 3.528s passed
getAnyOfArray2seq data()[181] 3.571s passed
getOfArray2seq data()[182] 3.582s passed
getAnyOfNPermInv data()[183] 3.599s passed
seqNPermRange data()[184] 3.588s passed
seqPermTrans data()[185] 3.642s passed
seqPermRefl data()[186] 3.644s passed
seqPermSplit data()[187] 3.677s passed
seqNPermRight data()[188] 3.655s passed
seqPermFromSwap data()[189] 3.605s passed
divResZero1 data()[18] 3.654s passed
seqPermTransAlt0 data()[190] 3.639s passed
seqPermTransAlt1 data()[191] 3.644s passed
seqPermTransAlt2 data()[192] 3.708s passed
seqPermTransAlt3 data()[193] 3.624s passed
seqPermForall data()[194] 3.652s passed
seqPermExists data()[195] 3.614s passed
schiffl_lemma_2 data()[196] 26.247s passed
schiffl_thm_1 data()[197] 4.422s passed
eqSameSeq data()[198] 3.561s passed
divResZero2 data()[19] 3.573s passed
eqTermCut data()[1] 4.375s passed
divResOne1 data()[20] 3.620s passed
divResOne2 data()[21] 3.625s passed
div_cancel1 data()[22] 3.508s passed
div_cancel2 data()[23] 3.491s passed
divAddMultDenom data()[24] 3.508s passed
divMinus data()[25] 3.626s passed
divMinusDenom data()[26] 3.782s passed
divLeastDPos data()[27] 3.811s passed
divLeastDNeg data()[28] 3.697s passed
divGreatestDPos data()[29] 3.712s passed
equivAllRight data()[2] 3.946s passed
divGreatestDNeg data()[30] 3.598s passed
divIncreasingPos data()[31] 3.471s passed
divIncreasingNeg data()[32] 3.479s passed
jdiv_zero data()[33] 3.464s passed
jdivPulloutMinusNum data()[34] 3.500s passed
jdivPulloutMinusDenom data()[35] 3.572s passed
jdiv_uniquePosPos data()[36] 3.480s passed
jdiv_uniquePosNeg data()[37] 3.459s passed
jdiv_uniqueNegPos data()[38] 3.593s passed
jdiv_uniqueNegNeg data()[39] 3.524s passed
irrflConcrete1 data()[3] 3.809s passed
jdivMultDenom1 data()[40] 3.525s passed
jdivMultDenom2 data()[41] 3.460s passed
mod_geZero data()[42] 3.515s passed
mod_lessDenom data()[43] 3.478s passed
jmod_NumPos data()[44] 3.610s passed
jmod_NumNeg data()[45] 3.475s passed
jmod_geZero data()[46] 3.480s passed
jmodNumZero data()[47] 3.678s passed
jmod_pulloutminusNum data()[48] 3.735s passed
jmod_pulloutminusDenom data()[49] 3.760s passed
irrflConcrete2 data()[4] 3.822s passed
jmodUnique1 data()[50] 3.726s passed
jmodUnique2 data()[51] 3.649s passed
intDivRem data()[52] 3.657s passed
jmodjmod data()[53] 3.673s passed
jmodDivisible data()[54] 3.650s passed
jmodDivisibleRep data()[55] 3.605s passed
jdivAddMultDenom data()[56] 3.736s passed
jmodAltZero data()[57] 3.547s passed
jmodAddMultDenomZero data()[58] 3.544s passed
polyDiv_zero data()[59] 3.485s passed
cancel_gtPos data()[5] 3.701s passed
polyMod_ltdivDenom data()[60] 3.484s passed
bsum_empty data()[61] 3.654s passed
bsum_induction_upper data()[62] 3.644s passed
bsum_induction_lower data()[63] 3.684s passed
bsum_num_of_bounds data()[64] 3.740s passed
bsum_num_of_bounds2 data()[65] 3.648s passed
bsum_induction_upper2 data()[66] 3.500s passed
bsum_induction_upper_concrete data()[67] 3.518s passed
bsum_induction_upper_concrete_2 data()[68] 3.756s passed
bsum_induction_upper2_concrete data()[69] 3.743s passed
cancel_gtNeg data()[6] 3.736s passed
bsum_induction_lower_concrete data()[70] 3.693s passed
bsum_induction_lower2 data()[71] 3.639s passed
bsum_induction_lower2_concrete data()[72] 3.584s passed
bsum_positive data()[73] 3.727s passed
bsum_upper_bound data()[74] 3.699s passed
bsum_lower_bound data()[75] 3.640s passed
bsum_positive_lower_bound_element data()[76] 3.656s passed
bsum_sub_same_index data()[77] 3.619s passed
bsum_less_same_index data()[78] 3.753s passed
bsum_equal_except_one_index data()[79] 3.578s passed
moduloIntIsInInt data()[7] 3.806s passed
bsum_num_of_is_max data()[80] 3.596s passed
bsum_num_of_is_max2 data()[81] 3.578s passed
bsum_num_of_is_max3 data()[82] 3.561s passed
bsum_num_of_is_max4 data()[83] 3.629s passed
bsum_num_of_lt_max data()[84] 3.699s passed
bsum_num_of_lt_max2 data()[85] 3.651s passed
bsum_num_of_lt_max3 data()[86] 3.645s passed
bsum_num_of_lt_max4 data()[87] 3.690s passed
bsum_num_of_gt0 data()[88] 3.782s passed
bsum_num_of_gt0_alt data()[89] 3.813s passed
moduloLongIsInLong data()[8] 3.816s passed
bsum_add_concrete data()[90] 3.638s passed
bprod_all_positive data()[91] 3.661s passed
bprod_split data()[92] 3.666s passed
powConcrete0 data()[93] 3.620s passed
powConcrete1 data()[94] 3.687s passed
powSplitFactor data()[95] 3.698s passed
powAdd data()[96] 3.614s passed
powMono data()[97] 3.596s passed
powMonoConcrete data()[98] 3.632s passed
powMonoConcreteRight data()[99] 3.603s passed
moduloShortIsInShort data()[9] 3.695s passed

Standard output

602        INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src/test/resources/testcase/dummyTrue.key 
628        DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 11.51ms 
854        INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
874        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)

1778       DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for Meta 
1780       DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for Meta 
1781       DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for Meta 
1781       DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for Meta 
3354       DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for JavaBigintExpression 
9068       DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 8.21s 
9151       INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof dummyTrue.key 
9190       DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 38.2ns 
9204       INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/firstOrder/Taclet_eqTermCut.proof 
9204       DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 159.61ns 
9208       INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
12446      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.24s 
12449      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: eqTermCut 
13540      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: eqTermCut 
13569      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 21.95ms 
13590      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/firstOrder/Taclet_equivAllRight.proof 
13590      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 178.91ns 
13597      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
16516      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.92s 
16516      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: equivAllRight 
17520      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: equivAllRight 
17534      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 10.17ms 
17537      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_irrflConcrete1.proof 
17537      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 408.22ns 
17539      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
20390      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.85s 
20391      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: irrflConcrete1 
21337      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: irrflConcrete1 
21344      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.69ms 
21347      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_irrflConcrete2.proof 
21347      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 404.52ns 
21349      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
24144      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.79s 
24145      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: irrflConcrete2 
25153      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: irrflConcrete2 
25166      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 7.41ms 
25170      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_cancel_gtPos.proof 
25171      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 452.12ns 
25172      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
27925      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.75s 
27926      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: cancel_gtPos 
28827      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: cancel_gtPos 
28867      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 36.96ms 
28872      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_cancel_gtNeg.proof 
28872      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 464.83ns 
28875      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
31642      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.77s 
31643      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: cancel_gtNeg 
32578      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: cancel_gtNeg 
32603      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 21.56ms 
32610      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intRulesIgnoringOF/Taclet_moduloIntIsInInt.proof 
32611      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 428.12ns 
32612      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
35494      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.88s 
35494      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: moduloIntIsInInt 
36410      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: moduloIntIsInInt 
36413      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 770.94ns 
36415      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intRulesIgnoringOF/Taclet_moduloLongIsInLong.proof 
36415      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 136.41ns 
36416      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
39299      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.88s 
39299      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: moduloLongIsInLong 
40221      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: moduloLongIsInLong 
40226      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 654.44ns 
40232      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intRulesIgnoringOF/Taclet_moduloShortIsInShort.proof 
40233      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 405.82ns 
40234      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
43054      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.82s 
43055      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: moduloShortIsInShort 
43922      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: moduloShortIsInShort 
43925      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 641.84ns 
43928      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intRulesIgnoringOF/Taclet_moduloByteIsInByte.proof 
43928      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 312.12ns 
43929      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
46636      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.71s 
46638      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: moduloByteIsInByte 
47506      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: moduloByteIsInByte 
47509      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 609.33ns 
47512      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intRulesIgnoringOF/Taclet_moduloCharIsInChar.proof 
47512      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 360.62ns 
47514      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
50265      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.75s 
50265      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: moduloCharIsInChar 
51138      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: moduloCharIsInChar 
51141      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 690.44ns 
51143      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_div_unique1.proof 
51143      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 220.01ns 
51144      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
54133      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.99s 
54133      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: div_unique1 
55004      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: div_unique1 
55042      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 34.14ms 
55048      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_div_unique2.proof 
55049      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 562.73ns 
55051      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
57862      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.81s 
57862      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: div_unique2 
58788      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: div_unique2 
58839      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 47.83ms 
58842      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_div_exists.proof 
58842      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 182.91ns 
58844      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
61575      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.73s 
61575      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: div_exists 
62469      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: div_exists 
62636      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 157.51ms 
62641      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_div_one.proof 
62641      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 424.92ns 
62643      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
65383      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.74s 
65384      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: div_one 
66276      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: div_one 
66282      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.83ms 
66285      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdiv_one.proof 
66285      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 337.32ns 
66287      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
68970      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.68s 
68971      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdiv_one 
69883      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdiv_one 
69887      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.5ms 
69890      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_div_zero.proof 
69890      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 342.72ns 
69892      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
72601      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.71s 
72601      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: div_zero 
73502      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: div_zero 
73551      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 43.74ms 
73553      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divResZero1.proof 
73554      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 412.32ns 
73555      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
76286      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.73s 
76287      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divResZero1 
77192      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divResZero1 
77205      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 10.26ms 
77207      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divResZero2.proof 
77207      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 208.71ns 
77208      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
79872      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.66s 
79872      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divResZero2 
80766      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divResZero2 
80778      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 9.19ms 
80779      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divResOne1.proof 
80779      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 93.2ns 
80780      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
83486      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.71s 
83486      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divResOne1 
84384      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divResOne1 
84398      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 10.69ms 
84400      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divResOne2.proof 
84400      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 216.21ns 
84401      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
87121      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.72s 
87121      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divResOne2 
88010      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divResOne2 
88023      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 10.79ms 
88026      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_div_cancel1.proof 
88027      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 879.24ns 
88029      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
90646      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.62s 
90647      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: div_cancel1 
91512      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: div_cancel1 
91531      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 14.86ms 
91533      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_div_cancel2.proof 
91534      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 379.32ns 
91535      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
94165      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.63s 
94166      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: div_cancel2 
95018      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: div_cancel2 
95021      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.31ms 
95024      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divAddMultDenom.proof 
95024      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 359.42ns 
95026      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
97598      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.57s 
97599      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divAddMultDenom 
98494      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divAddMultDenom 
98530      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 29.21ms 
98533      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divMinus.proof 
98533      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 343.72ns 
98534      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
101216     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.68s 
101216     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divMinus 
102073     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divMinus 
102155     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 61.19ms 
102160     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divMinusDenom.proof 
102161     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 512.03ns 
102162     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
104939     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.78s 
104940     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divMinusDenom 
105894     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divMinusDenom 
105939     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 39.14ms 
105944     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divLeastDPos.proof 
105944     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 495.23ns 
105946     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
108821     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.88s 
108824     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divLeastDPos 
109744     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divLeastDPos 
109752     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 5.2ms 
109753     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divLeastDNeg.proof 
109753     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 106.51ns 
109754     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
112544     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.79s 
112545     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divLeastDNeg 
113437     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divLeastDNeg 
113450     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 10.18ms 
113451     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divGreatestDPos.proof 
113451     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 106.71ns 
113452     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
116237     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.78s 
116237     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divGreatestDPos 
117142     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divGreatestDPos 
117161     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 13.12ms 
117165     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divGreatestDNeg.proof 
117166     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 1.09ms 
117168     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
119892     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.72s 
119893     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divGreatestDNeg 
120754     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divGreatestDNeg 
120761     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.63ms 
120763     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divIncreasingPos.proof 
120763     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 298.22ns 
120764     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
123357     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.59s 
123358     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divIncreasingPos 
124224     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divIncreasingPos 
124231     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.94ms 
124234     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divIncreasingNeg.proof 
124234     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 294.62ns 
124235     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
126809     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.57s 
126809     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divIncreasingNeg 
127698     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divIncreasingNeg 
127709     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 7.35ms 
127713     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdiv_zero.proof 
127713     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 106.2ns 
127714     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
130314     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.6s 
130314     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdiv_zero 
131171     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdiv_zero 
131175     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.68ms 
131177     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdivPulloutMinusNum.proof 
131177     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 92.61ns 
131178     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
133800     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.62s 
133800     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdivPulloutMinusNum 
134665     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdivPulloutMinusNum 
134675     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 7.71ms 
134677     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdivPulloutMinusDenom.proof 
134677     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 111.11ns 
134678     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
137301     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.62s 
137301     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdivPulloutMinusDenom 
138185     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdivPulloutMinusDenom 
138246     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 47.02ms 
138249     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdiv_uniquePosPos.proof 
138249     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 197.11ns 
138250     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
140808     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.56s 
140808     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdiv_uniquePosPos 
141707     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdiv_uniquePosPos 
141727     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 14.14ms 
141729     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdiv_uniquePosNeg.proof 
141729     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 213.11ns 
141731     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
144323     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.59s 
144323     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdiv_uniquePosNeg 
145171     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdiv_uniquePosNeg 
145186     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 12.72ms 
145188     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdiv_uniqueNegPos.proof 
145188     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 127.41ns 
145189     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
147869     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.68s 
147869     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdiv_uniqueNegPos 
148753     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdiv_uniqueNegPos 
148779     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 21.34ms 
148781     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdiv_uniqueNegNeg.proof 
148782     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 316.72ns 
148783     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
151408     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.63s 
151409     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdiv_uniqueNegNeg 
152288     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdiv_uniqueNegNeg 
152303     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 12.02ms 
152304     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdivMultDenom1.proof 
152304     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 110.21ns 
152305     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
154907     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.6s 
154907     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdivMultDenom1 
155792     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdivMultDenom1 
155828     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 30.95ms 
155830     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdivMultDenom2.proof 
155830     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 113.51ns 
155831     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
158410     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.58s 
158411     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdivMultDenom2 
159285     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdivMultDenom2 
159288     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.13ms 
159290     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_mod_geZero.proof 
159290     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 84.2ns 
159291     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
161944     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.65s 
161944     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: mod_geZero 
162799     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: mod_geZero 
162804     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.36ms 
162805     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_mod_lessDenom.proof 
162805     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 324.22ns 
162806     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
165430     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.62s 
165430     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: mod_lessDenom 
166274     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: mod_lessDenom 
166281     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 5.41ms 
166283     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmod_NumPos.proof 
166283     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 78.1ns 
166284     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
168990     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.71s 
168990     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmod_NumPos 
169883     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmod_NumPos 
169891     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 5.98ms 
169892     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmod_NumNeg.proof 
169893     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 90.81ns 
169893     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
172523     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.63s 
172524     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmod_NumNeg 
173349     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmod_NumNeg 
173366     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 14.3ms 
173367     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmod_geZero.proof 
173368     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 81.7ns 
173368     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
175988     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.62s 
175989     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmod_geZero 
176839     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmod_geZero 
176846     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.84ms 
176849     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmodNumZero.proof 
176849     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 314.42ns 
176850     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
179623     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.77s 
179624     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmodNumZero 
180520     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmodNumZero 
180524     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.37ms 
180527     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmod_pulloutminusNum.proof 
180528     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 1.18ms 
180529     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
183322     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.79s 
183322     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmod_pulloutminusNum 
184250     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmod_pulloutminusNum 
184257     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.3ms 
184262     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmod_pulloutminusDenom.proof 
184262     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 122.81ns 
184263     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
187071     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.81s 
187071     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmod_pulloutminusDenom 
188009     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmod_pulloutminusDenom 
188021     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 9.56ms 
188022     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmodUnique1.proof 
188022     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 112.31ns 
188028     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
190795     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.77s 
190795     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmodUnique1 
191682     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmodUnique1 
191746     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 55.01ms 
191748     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmodUnique2.proof 
191748     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 110.21ns 
191749     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
194426     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.68s 
194427     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmodUnique2 
195310     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmodUnique2 
195395     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 74.77ms 
195398     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_intDivRem.proof 
195398     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 365.82ns 
195399     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
198141     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.74s 
198141     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: intDivRem 
199048     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: intDivRem 
199052     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.45ms 
199054     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmodjmod.proof 
199054     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 275.01ns 
199056     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
201786     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.73s 
201786     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmodjmod 
202693     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmodjmod 
202725     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 28.11ms 
202727     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmodDivisible.proof 
202727     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 102.2ns 
202728     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
205428     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.7s 
205428     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmodDivisible 
206340     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmodDivisible 
206369     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 25.34ms 
206377     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmodDivisibleRep.proof 
206377     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 111.51ns 
206378     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
209067     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.69s 
209067     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmodDivisibleRep 
209975     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmodDivisibleRep 
209980     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.28ms 
209982     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdivAddMultDenom.proof 
209982     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 75.1ns 
209983     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
212686     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.7s 
212686     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdivAddMultDenom 
213588     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdivAddMultDenom 
213716     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 113.36ms 
213718     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmodAltZero.proof 
213718     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 169.61ns 
213719     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
216359     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.64s 
216359     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmodAltZero 
217245     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmodAltZero 
217263     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 15.59ms 
217266     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmodAddMultDenomZero.proof 
217267     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 335.42ns 
217269     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
219911     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.64s 
219911     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmodAddMultDenomZero 
220801     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmodAddMultDenomZero 
220808     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.89ms 
220809     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_polyDiv_zero.proof 
220809     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 73ns 
220810     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
223431     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.62s 
223431     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: polyDiv_zero 
224277     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: polyDiv_zero 
224292     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 12.03ms 
224293     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_polyMod_ltdivDenom.proof 
224294     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 82.4ns 
224294     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
226915     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.62s 
226916     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: polyMod_ltdivDenom 
227763     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: polyMod_ltdivDenom 
227776     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 5.29ms 
227778     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_empty.proof 
227778     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 93.81ns 
227779     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
230536     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.76s 
230536     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_empty 
231426     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_empty 
231430     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.55ms 
231432     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_induction_upper.proof 
231432     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 88.41ns 
231433     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
234183     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.75s 
234183     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_upper 
235070     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_induction_upper 
235075     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.3ms 
235076     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_induction_lower.proof 
235076     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 81.81ns 
235077     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
237849     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.77s 
237849     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_lower 
238740     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_induction_lower 
238758     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 13.05ms 
238762     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_bounds.proof 
238764     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 1.56ms 
238765     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
241579     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.81s 
241580     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_bounds 
242487     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_bounds 
242500     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 9.8ms 
242502     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_bounds2.proof 
242502     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 92.5ns 
242503     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
245222     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.72s 
245223     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_bounds2 
246135     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_bounds2 
246148     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 10.45ms 
246149     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_induction_upper2.proof 
246149     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 70.8ns 
246150     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
248778     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.63s 
248778     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_upper2 
249645     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_induction_upper2 
249648     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.1ms 
249650     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_induction_upper_concrete.proof 
249650     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 87.11ns 
249651     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
252292     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.64s 
252292     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_upper_concrete 
253162     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_induction_upper_concrete 
253166     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.58ms 
253167     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_induction_upper_concrete_2.proof 
253167     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 92.2ns 
253168     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
255992     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.82s 
255992     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_upper_concrete_2 
256917     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_induction_upper_concrete_2 
256922     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.19ms 
256923     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_induction_upper2_concrete.proof 
256924     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 94.31ns 
256924     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
259713     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.79s 
259714     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_upper2_concrete 
260662     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_induction_upper2_concrete 
260665     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 954.75ns 
260668     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_induction_lower_concrete.proof 
260668     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 275.71ns 
260669     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
263435     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.77s 
263436     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_lower_concrete 
264356     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_induction_lower_concrete 
264358     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 547.13ns 
264360     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_induction_lower2.proof 
264360     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 140.11ns 
264361     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
267082     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.72s 
267082     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_lower2 
267993     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_induction_lower2 
267997     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.73ms 
267998     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_induction_lower2_concrete.proof 
267998     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 81.2ns 
267999     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
270688     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.69s 
270688     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_lower2_concrete 
271578     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_induction_lower2_concrete 
271581     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 787.34ns 
271582     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_positive.proof 
271582     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 65.81ns 
271583     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
274316     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.73s 
274316     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_positive 
275243     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_positive 
275308     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 57.98ms 
275310     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_upper_bound.proof 
275310     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 102.41ns 
275311     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
278079     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.77s 
278079     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_upper_bound 
278977     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_upper_bound 
279008     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 26.99ms 
279009     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_lower_bound.proof 
279009     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 76.61ns 
279010     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
281731     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.72s 
281731     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_lower_bound 
282622     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_lower_bound 
282647     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 21.99ms 
282649     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_positive_lower_bound_element.proof 
282649     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 88.91ns 
282650     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
285390     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.74s 
285390     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_positive_lower_bound_element 
286269     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_positive_lower_bound_element 
286303     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 28.67ms 
286304     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_sub_same_index.proof 
286304     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 94.11ns 
286305     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
289021     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.72s 
289021     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_sub_same_index 
289899     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_sub_same_index 
289922     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 18.91ms 
289923     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_less_same_index.proof 
289923     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 91.81ns 
289924     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
292703     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.78s 
292703     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_less_same_index 
293635     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_less_same_index 
293675     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 33.52ms 
293676     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_equal_except_one_index.proof 
293676     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 88.11ns 
293677     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
296376     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.7s 
296377     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_equal_except_one_index 
297233     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_equal_except_one_index 
297253     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 16.42ms 
297255     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_is_max.proof 
297255     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 84.21ns 
297256     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
299962     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.71s 
299962     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_is_max 
300835     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_is_max 
300850     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 11.86ms 
300851     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_is_max2.proof 
300851     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 83.91ns 
300852     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
303564     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.71s 
303564     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_is_max2 
304410     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_is_max2 
304427     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 13.68ms 
304429     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_is_max3.proof 
304429     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 83.71ns 
304430     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
307091     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.66s 
307091     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_is_max3 
307975     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_is_max3 
307988     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 10.44ms 
307989     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_is_max4.proof 
307990     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 85.41ns 
307990     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
310664     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.67s 
310664     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_is_max4 
311598     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_is_max4 
311617     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 15.83ms 
311619     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_lt_max.proof 
311619     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 175.61ns 
311620     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
314393     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.77s 
314393     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_lt_max 
315298     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_lt_max 
315316     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 14.67ms 
315317     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_lt_max2.proof 
315318     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 91.11ns 
315318     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
318055     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.74s 
318056     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_lt_max2 
318949     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_lt_max2 
318967     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 14.25ms 
318968     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_lt_max3.proof 
318968     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 72.5ns 
318969     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
321670     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.7s 
321670     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_lt_max3 
322596     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_lt_max3 
322613     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 13.42ms 
322614     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_lt_max4.proof 
322614     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 85.91ns 
322615     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
325354     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.74s 
325354     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_lt_max4 
326286     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_lt_max4 
326302     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 12.54ms 
326304     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_gt0.proof 
326304     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 88.11ns 
326304     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
329111     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.81s 
329111     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_gt0 
330058     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_gt0 
330084     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 21.92ms 
330093     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_gt0_alt.proof 
330093     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 397.33ns 
330094     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
332941     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.85s 
332941     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_gt0_alt 
333887     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_gt0_alt 
333904     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 13.66ms 
333906     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_add_concrete.proof 
333906     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 85.81ns 
333907     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
336645     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.74s 
336645     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_add_concrete 
337536     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_add_concrete 
337542     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.13ms 
337545     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bprod/Taclet_bprod_all_positive.proof 
337545     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 218.82ns 
337546     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
340271     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.72s 
340271     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bprod_all_positive 
341191     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bprod_all_positive 
341204     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 9.67ms 
341205     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bprod/Taclet_bprod_split.proof 
341205     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 68.61ns 
341206     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
343985     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.78s 
343985     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bprod_split 
344866     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bprod_split 
344870     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.7ms 
344871     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powConcrete0.proof 
344871     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 71.31ns 
344872     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
347571     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.7s 
347571     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powConcrete0 
348481     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powConcrete0 
348490     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.44ms 
348491     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powConcrete1.proof 
348491     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 79.21ns 
348492     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
351279     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.79s 
351279     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powConcrete1 
352174     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powConcrete1 
352177     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 726.15ns 
352178     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powSplitFactor.proof 
352178     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 62.41ns 
352179     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
354975     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.8s 
354975     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powSplitFactor 
355868     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powSplitFactor 
355874     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.44ms 
355875     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powAdd.proof 
355875     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 74.61ns 
355876     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
358591     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.71s 
358591     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powAdd 
359483     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powAdd 
359489     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.54ms 
359490     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powMono.proof 
359490     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 60.7ns 
359491     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
362200     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.71s 
362201     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powMono 
363073     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powMono 
363084     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 8.29ms 
363086     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powMonoConcrete.proof 
363086     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 75.91ns 
363087     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
365819     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.73s 
365819     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powMonoConcrete 
366713     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powMonoConcrete 
366717     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.85ms 
366718     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powMonoConcreteRight.proof 
366718     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 56.01ns 
366719     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
369444     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.73s 
369445     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powMonoConcreteRight 
370317     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powMonoConcreteRight 
370320     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 476.74ns 
370321     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powPositive.proof 
370321     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 74.21ns 
370322     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
372975     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.65s 
372976     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powPositive 
373867     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powPositive 
373874     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.34ms 
373876     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powPositiveConcrete.proof 
373876     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 233.52ns 
373877     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
376597     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.72s 
376597     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powPositiveConcrete 
377492     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powPositiveConcrete 
377495     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 556.43ns 
377496     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powGeq1Concrete.proof 
377496     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 81.91ns 
377497     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
380143     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.65s 
380143     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powGeq1Concrete 
381041     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powGeq1Concrete 
381043     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 543.34ns 
381045     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_pow2InIntLower.proof 
381046     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 184.31ns 
381046     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
383741     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.69s 
383741     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: pow2InIntLower 
384637     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: pow2InIntLower 
384639     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 594.24ns 
384640     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_pow2InIntUpper.proof 
384640     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 57.4ns 
384641     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
387366     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.73s 
387366     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: pow2InIntUpper 
388261     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: pow2InIntUpper 
388265     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.96ms 
388266     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logSelfConcrete.proof 
388266     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 57.4ns 
388267     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
390957     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.69s 
390957     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logSelfConcrete 
391866     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logSelfConcrete 
391875     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 5.68ms 
391876     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_log1Concrete.proof 
391876     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 86.71ns 
391877     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
394643     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.77s 
394644     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: log1Concrete 
395582     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: log1Concrete 
395586     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.96ms 
395587     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logProduct.proof 
395587     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 73.81ns 
395588     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
398396     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.81s 
398396     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logProduct 
399323     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logProduct 
399329     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.02ms 
399330     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logTimesBaseConcrete.proof 
399330     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 73.41ns 
399331     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
402047     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.72s 
402047     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logTimesBaseConcrete 
402944     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logTimesBaseConcrete 
402955     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 8.27ms 
402956     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logProdIdentity.proof 
402956     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 117.91ns 
402957     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
405642     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.69s 
405643     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logProdIdentity 
406605     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logProdIdentity 
406619     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 10.75ms 
406621     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logProdIdentityConcrete.proof 
406621     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 132.71ns 
406622     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
409324     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.7s 
409324     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logProdIdentityConcrete 
410245     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logProdIdentityConcrete 
410249     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.73ms 
410251     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logPowIdentity.proof 
410251     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 74.31ns 
410252     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
413015     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.76s 
413016     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logPowIdentity 
413983     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logPowIdentity 
413986     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.1ms 
413988     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logPowIdentityConcrete.proof 
413988     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 56ns 
413988     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
416775     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.79s 
416775     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logPowIdentityConcrete 
417675     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logPowIdentityConcrete 
417679     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.76ms 
417680     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logPositive.proof 
417680     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 53.8ns 
417681     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
420441     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.76s 
420441     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logPositive 
421327     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logPositive 
421344     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 11.59ms 
421347     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logPositiveConcrete.proof 
421347     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 263.92ns 
421348     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
424110     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.76s 
424111     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logPositiveConcrete 
424994     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logPositiveConcrete 
424999     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 335.22ns 
425001     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logMono.proof 
425001     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 127.11ns 
425002     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
427765     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.76s 
427765     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logMono 
428645     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logMono 
428676     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 25.65ms 
428677     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logMonoConcrete.proof 
428678     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 83.11ns 
428678     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
431437     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.76s 
431437     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logMonoConcrete 
432324     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logMonoConcrete 
432328     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.66ms 
432329     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powLogLess.proof 
432329     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 58.4ns 
432330     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
435112     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.78s 
435113     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powLogLess 
436008     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powLogLess 
436065     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 52.71ms 
436068     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powLogMore2.proof 
436068     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 244.02ns 
436069     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
438807     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.74s 
438807     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powLogMore2 
439715     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powLogMore2 
439730     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 12.77ms 
439732     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logLessThanPow.proof 
439732     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 76.11ns 
439733     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
442458     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.73s 
442459     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logLessThanPow 
443372     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logLessThanPow 
443392     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 16.5ms 
443393     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logLessThanPowConcrete.proof 
443394     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 62ns 
443394     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
446131     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.74s 
446131     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logLessThanPowConcrete 
447069     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logLessThanPowConcrete 
447071     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 478.53ns 
447074     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logSqueeze.proof 
447074     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 233.72ns 
447075     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
449807     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.73s 
449807     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logSqueeze 
450695     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logSqueeze 
450700     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.6ms 
450702     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/booleanRules/Taclet_ifthenelse_equals.proof 
450702     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 59.8ns 
450702     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
453301     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.6s 
453302     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: ifthenelse_equals 
454183     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: ifthenelse_equals 
454186     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.49ms 
454189     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/booleanRules/Taclet_ifthenelse_equals_1.proof 
454189     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 226.62ns 
454190     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
456830     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.64s 
456831     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: ifthenelse_equals_1 
457700     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: ifthenelse_equals_1 
457703     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 822.95ns 
457704     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/booleanRules/Taclet_ifthenelse_equals_2.proof 
457704     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 57.4ns 
457705     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
460270     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.56s 
460270     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: ifthenelse_equals_2 
461152     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: ifthenelse_equals_2 
461154     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 719.55ns 
461156     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/locSet/Taclet_disjointWithSingleton1.proof 
461156     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 198.21ns 
461157     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
463732     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.58s 
463732     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: disjointWithSingleton1 
464604     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: disjointWithSingleton1 
464607     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.04ms 
464608     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/locSet/Taclet_disjointWithSingleton2.proof 
464608     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 57.4ns 
464609     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
467299     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.69s 
467299     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: disjointWithSingleton2 
468219     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: disjointWithSingleton2 
468222     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.16ms 
468224     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/locSet/Taclet_disjointArrayRanges.proof 
468224     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 77.41ns 
468225     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
471024     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.8s 
471024     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: disjointArrayRanges 
471898     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: disjointArrayRanges 
471906     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 5.74ms 
471907     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/locSet/Taclet_disjointArrayRangeAllFields1.proof 
471907     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 49.2ns 
471908     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
474515     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.61s 
474516     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: disjointArrayRangeAllFields1 
475371     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: disjointArrayRangeAllFields1 
475379     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 5.04ms 
475386     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/locSet/Taclet_disjointArrayRangeAllFields2.proof 
475386     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 66.5ns 
475387     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
477965     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.58s 
477965     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: disjointArrayRangeAllFields2 
478815     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: disjointArrayRangeAllFields2 
478822     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.86ms 
478823     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqSelfDefinition.proof 
478823     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 66.81ns 
478824     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
481521     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.7s 
481521     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqSelfDefinition 
482433     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqSelfDefinition 
482447     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 11.7ms 
482449     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqOutsideValue.proof 
482449     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 76.2ns 
482449     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
485108     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.66s 
485108     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqOutsideValue 
486034     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqOutsideValue 
486038     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.97ms 
486040     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_castedGetAny.proof 
486040     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 79.91ns 
486041     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
488666     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.63s 
488667     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: castedGetAny 
489580     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: castedGetAny 
489584     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.42ms 
489585     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqGetAlphaCast.proof 
489585     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 65.6ns 
489586     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
492304     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.72s 
492304     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqGetAlphaCast 
493236     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqGetAlphaCast 
493239     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 854.96ns 
493240     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqSingleton.proof 
493240     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 69.7ns 
493241     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
495970     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.73s 
495970     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqSingleton 
496907     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqSingleton 
496910     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.05ms 
496911     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqSingletonConcrete.proof 
496911     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 70.5ns 
496912     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
499660     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.75s 
499660     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqSingletonConcrete 
500557     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqSingletonConcrete 
500560     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.1ms 
500561     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqConcat.proof 
500561     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 70.91ns 
500562     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
503279     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.72s 
503279     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqConcat 
504236     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqConcat 
504245     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 7.31ms 
504247     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqSub.proof 
504247     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 82.81ns 
504248     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
507082     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.83s 
507082     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqSub 
507988     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqSub 
507990     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.22ms 
507992     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqReverse.proof 
507992     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 69ns 
507993     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
510665     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.67s 
510665     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqReverse 
511586     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqReverse 
511592     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.91ms 
511593     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqEmpty.proof 
511593     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 72.3ns 
511594     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
514293     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.7s 
514293     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqEmpty 
515204     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqEmpty 
515206     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 851.25ns 
515208     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqSingleton.proof 
515208     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 59.4ns 
515208     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
517899     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.69s 
517900     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqSingleton 
518761     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqSingleton 
518763     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 646.34ns 
518764     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqConcat.proof 
518764     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 66.4ns 
518765     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
521369     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.6s 
521370     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqConcat 
522230     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqConcat 
522233     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.47ms 
522235     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqSub.proof 
522235     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 69.4ns 
522236     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
524769     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.53s 
524769     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqSub 
525624     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqSub 
525627     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 778.45ns 
525628     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqReverse.proof 
525628     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 69.2ns 
525629     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
528168     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.54s 
528168     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqReverse 
529047     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqReverse 
529050     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.06ms 
529051     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_equalityToSeqGetAndSeqLenLeft.proof 
529051     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 70.8ns 
529052     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
531669     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.62s 
531669     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: equalityToSeqGetAndSeqLenLeft 
532519     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: equalityToSeqGetAndSeqLenLeft 
532521     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 874.26ns 
532522     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_equalityToSeqGetAndSeqLenRight.proof 
532522     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 68.3ns 
532523     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
535155     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.63s 
535155     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: equalityToSeqGetAndSeqLenRight 
536056     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: equalityToSeqGetAndSeqLenRight 
536061     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.2ms 
536062     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqSingletonEQ.proof 
536062     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 79.7ns 
536063     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
538793     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.73s 
538793     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqSingletonEQ 
539723     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqSingletonEQ 
539726     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 904.96ns 
539727     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqConcatEQ.proof 
539727     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 72.2ns 
539728     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
542411     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.68s 
542411     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqConcatEQ 
543281     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqConcatEQ 
543290     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 6.89ms 
543292     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqSubEQ.proof 
543292     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 56.3ns 
543292     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
545909     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.62s 
545909     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqSubEQ 
546765     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqSubEQ 
546767     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 605.54ns 
546768     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqReverseEQ.proof 
546768     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 55ns 
546769     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
549405     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.64s 
549405     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqReverseEQ 
550270     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqReverseEQ 
550276     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.81ms 
550277     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqEmptyEQ.proof 
550277     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 64ns 
550278     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
552890     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.61s 
552890     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqEmptyEQ 
553766     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqEmptyEQ 
553768     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 826.85ns 
553769     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqSingletonEQ.proof 
553769     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 52.2ns 
553770     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
556329     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.56s 
556330     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqSingletonEQ 
557181     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqSingletonEQ 
557183     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 663.74ns 
557184     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqConcatEQ.proof 
557184     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 65.31ns 
557185     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
559799     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.61s 
559799     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqConcatEQ 
560685     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqConcatEQ 
560689     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.88ms 
560690     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqSubEQ.proof 
560691     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 55.4ns 
560691     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
563241     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.55s 
563241     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqSubEQ 
564096     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqSubEQ 
564098     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 957.16ns 
564100     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqReverseEQ.proof 
564100     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 67.9ns 
564100     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
566751     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.65s 
566751     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqReverseEQ 
567599     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqReverseEQ 
567601     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.21ms 
567603     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqDefEQ.proof 
567603     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 55.1ns 
567603     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
570203     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.6s 
570203     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqDefEQ 
571067     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqDefEQ 
571070     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.15ms 
571072     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqDefEQ.proof 
571072     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 50ns 
571072     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
573685     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.61s 
573685     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqDefEQ 
574552     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqDefEQ 
574556     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.34ms 
574557     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqConcatWithSeqEmpty1.proof 
574557     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 68.2ns 
574558     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
577142     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.58s 
577142     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqConcatWithSeqEmpty1 
577980     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqConcatWithSeqEmpty1 
577987     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 5.25ms 
577988     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqConcatWithSeqEmpty2.proof 
577988     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 61.6ns 
577989     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
580552     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.56s 
580553     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqConcatWithSeqEmpty2 
581451     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqConcatWithSeqEmpty2 
581459     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 5.91ms 
581461     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqReverseOfSeqEmpty.proof 
581461     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 66.7ns 
581462     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
584020     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.56s 
584020     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqReverseOfSeqEmpty 
584889     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqReverseOfSeqEmpty 
584895     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.35ms 
584896     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_subSeqComplete.proof 
584896     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 57.3ns 
584897     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
587482     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.59s 
587482     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: subSeqComplete 
588338     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: subSeqComplete 
588343     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4ms 
588345     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_subSeqTailR.proof 
588345     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 64.8ns 
588346     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
590975     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.63s 
590975     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: subSeqTailR 
591956     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: subSeqTailR 
591968     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 9.15ms 
591969     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_subSeqTailL.proof 
591969     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 74.61ns 
591970     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
594773     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.8s 
594773     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: subSeqTailL 
595709     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: subSeqTailL 
595721     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 8.97ms 
595722     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_subSeqTailEQR.proof 
595722     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 73.2ns 
595723     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
598396     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.67s 
598397     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: subSeqTailEQR 
599295     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: subSeqTailEQR 
599308     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 10.11ms 
599309     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_subSeqTailEQL.proof 
599309     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 67.31ns 
599310     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
601956     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.65s 
601956     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: subSeqTailEQL 
602896     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: subSeqTailEQL 
602904     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 5.82ms 
602906     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDef_split.proof 
602906     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 80.11ns 
602907     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
605747     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.84s 
605747     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_split 
606678     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDef_split 
606701     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 19.21ms 
606703     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDef_induction_upper.proof 
606703     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 68.7ns 
606704     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
609587     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.88s 
609587     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_induction_upper 
610525     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDef_induction_upper 
610550     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 20.91ms 
610552     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDef_induction_upper_concrete.proof 
610552     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 83ns 
610553     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
613371     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.82s 
613371     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_induction_upper_concrete 
614276     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDef_induction_upper_concrete 
614302     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 22.16ms 
614305     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDef_induction_lower.proof 
614310     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 5.18ms 
614311     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
617057     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.75s 
617057     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_induction_lower 
617947     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDef_induction_lower 
617968     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 17.18ms 
617970     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDef_induction_lower_concrete.proof 
617970     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 79.41ns 
617971     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
620680     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.71s 
620680     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_induction_lower_concrete 
621582     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDef_induction_lower_concrete 
621604     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 17.62ms 
621605     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDef_split_in_three.proof 
621605     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 67ns 
621606     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
624317     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.71s 
624318     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_split_in_three 
625199     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDef_split_in_three 
625251     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 44.33ms 
625253     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDef_empty.proof 
625253     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 76.6ns 
625254     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
627954     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.7s 
627954     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_empty 
628862     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDef_empty 
628867     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.98ms 
628868     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDef_one_summand.proof 
628868     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 58.9ns 
628869     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
631559     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.69s 
631559     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_one_summand 
632477     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDef_one_summand 
632482     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.31ms 
632484     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDef_lower_equals_upper.proof 
632484     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 73.41ns 
632485     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
635138     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.65s 
635139     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_lower_equals_upper 
636094     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDef_lower_equals_upper 
636098     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.08ms 
636099     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDefOfSeq.proof 
636099     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 74ns 
636100     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
639021     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.92s 
639021     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDefOfSeq 
640018     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDefOfSeq 
640033     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 10.93ms 
640034     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqSelfDefinitionEQ2.proof 
640035     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 62.2ns 
640035     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
642701     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.67s 
642701     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqSelfDefinitionEQ2 
643588     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqSelfDefinitionEQ2 
643594     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.29ms 
643596     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_indexOfSeqSingleton.proof 
643596     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 67.5ns 
643596     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
646241     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.64s 
646241     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: indexOfSeqSingleton 
647109     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: indexOfSeqSingleton 
647112     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.37ms 
647114     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_indexOfSeqConcatFirst.proof 
647114     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 77.3ns 
647114     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
649761     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.65s 
649761     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: indexOfSeqConcatFirst 
650617     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: indexOfSeqConcatFirst 
650627     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 7.96ms 
650629     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_indexOfSeqConcatSecond.proof 
650629     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 72.3ns 
650629     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
653266     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.64s 
653266     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: indexOfSeqConcatSecond 
654183     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: indexOfSeqConcatSecond 
654194     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 8.39ms 
654196     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_indexOfSeqSub.proof 
654196     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 68.4ns 
654197     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
656818     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.62s 
656818     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: indexOfSeqSub 
657714     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: indexOfSeqSub 
657729     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 11.1ms 
657730     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfArray2seq.proof 
657730     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 59.9ns 
657731     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
660369     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.64s 
660369     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfArray2seq 
661253     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfArray2seq 
661256     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 971.46ns 
661257     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getAnyOfArray2seq.proof 
661257     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 51.7ns 
661258     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
663939     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.68s 
663939     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getAnyOfArray2seq 
664824     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getAnyOfArray2seq 
664827     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.83ms 
664829     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfArray2seq.proof 
664829     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 76.81ns 
664829     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
667501     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.67s 
667501     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfArray2seq 
668403     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfArray2seq 
668409     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.92ms 
668410     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_getAnyOfNPermInv.proof 
668410     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 68.1ns 
668411     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
671072     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.66s 
671072     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getAnyOfNPermInv 
672003     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getAnyOfNPermInv 
672008     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.1ms 
672009     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqNPermRange.proof 
672009     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 67.1ns 
672010     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
674640     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.63s 
674640     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqNPermRange 
675550     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqNPermRange 
675597     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 39.25ms 
675598     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermTrans.proof 
675598     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 78.41ns 
675599     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
678303     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.7s 
678303     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermTrans 
679218     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermTrans 
679238     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 16.23ms 
679239     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermRefl.proof 
679240     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 61.9ns 
679240     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
681941     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.7s 
681941     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermRefl 
682870     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermRefl 
682883     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 10.35ms 
682884     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermSplit.proof 
682884     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 76.91ns 
682885     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
685603     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.72s 
685603     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermSplit 
686558     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermSplit 
686560     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 273.72ns 
686561     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqNPermRight.proof 
686561     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 57.8ns 
686562     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
689203     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.64s 
689204     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqNPermRight 
690113     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqNPermRight 
690214     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 85.99ms 
690215     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermFromSwap.proof 
690216     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 80.61ns 
690216     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
692865     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.65s 
692865     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermFromSwap 
693780     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermFromSwap 
693819     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 33.05ms 
693821     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermTransAlt0.proof 
693821     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 134.61ns 
693822     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
696544     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.72s 
696544     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermTransAlt0 
697456     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermTransAlt0 
697458     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 203.91ns 
697459     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermTransAlt1.proof 
697460     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 58.7ns 
697460     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
700156     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.7s 
700156     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermTransAlt1 
701101     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermTransAlt1 
701103     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 288.72ns 
701104     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermTransAlt2.proof 
701104     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 74.3ns 
701105     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
703882     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.78s 
703882     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermTransAlt2 
704808     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermTransAlt2 
704810     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 205.61ns 
704812     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermTransAlt3.proof 
704812     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 57.5ns 
704812     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
707530     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.72s 
707531     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermTransAlt3 
708432     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermTransAlt3 
708434     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 342.52ns 
708435     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermForall.proof 
708435     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 64.9ns 
708436     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
711090     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.65s 
711090     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermForall 
711969     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermForall 
712072     INFO  Test worker     d.u.i.k.s.SMTFocusResults Analyzing unsat core: (L_1 L_3 L_4) 
712086     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 114ms 
712089     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermExists.proof 
712089     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 99.31ns 
712090     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
714751     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.66s 
714752     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermExists 
715645     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermExists 
715700     INFO  Test worker     d.u.i.k.s.SMTFocusResults Analyzing unsat core: (L_1 L_3 L_5 L_6 L_7) 
715701     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 53.3ms 
715703     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm2/Taclet_schiffl_lemma_2.proof 
715703     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 61.9ns 
715704     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
718355     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.65s 
718356     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: schiffl_lemma_2 
719220     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: schiffl_lemma_2 
719222     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.1ns 
719253     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 1: 'macro split-prop' on goal 0 (script from line 49) 
719304     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 2: 'rule allRight' on goal 3 (script from line 50) 
719324     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 3: 'rule allRight' on goal 4 (script from line 51) 
719331     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 4: 'macro split-prop' on goal 5 (script from line 52) 
719347     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 5: 'rule 'seqPermDefLeft'' on goal 11 (script from line 53) 
719349     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 6: 'rule 'andLeft'' on goal 12 (script from line 54) 
719351     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 7: 'rule 'exLeft'' on goal 13 (script from line 55) 
719352     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 8: 'macro split-prop' on goal 14 (script from line 56) 
719358     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 9: 'rule  seqNPermRange' on goal 16 (script from line 58) 
719361     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 10: 'instantiate var=iv with='v_x_0' occ=1' on goal 17 (script from line 59) 
719364     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 11: 'rule impLeft' on goal 18 (script from line 60) 
719367     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 12: 'tryclose branch' on goal 19 (script from line 61) 
719624     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 13: 'rule andLeft' on goal 20 (script from line 62) 
719625     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 14: 'rule andLeft' on goal 97 (script from line 63) 
719628     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 15: 'instantiate var=iv with='v_y_0' occ=1' on goal 98 (script from line 65) 
719628     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 16: 'rule impLeft' on goal 99 (script from line 66) 
719630     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 17: 'tryclose branch' on goal 100 (script from line 67) 
719785     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 18: 'rule andLeft' on goal 101 (script from line 68) 
719786     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 19: 'rule andLeft' on goal 188 (script from line 69) 
719790     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 20: 'rule seqNPermDefLeft' on goal 189 (script from line 71) 
719791     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 21: 'instantiate var=iv with='v_x_0' occ=2' on goal 190 (script from line 72) 
719793     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 22: 'rule impLeft' on goal 191 (script from line 73) 
719796     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 23: 'tryclose branch' on goal 192 (script from line 74) 
719981     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 24: 'rule exLeft' on goal 193 (script from line 75) 
719982     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 25: 'rule andLeft' on goal 310 (script from line 76) 
719984     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 26: 'rule andLeft' on goal 311 (script from line 77) 
719985     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 27: 'instantiate hide var=iv with='v_y_0' occ=2' on goal 312 (script from line 79) 
719985     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 28: 'rule impLeft' on goal 313 (script from line 80) 
719986     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 29: 'tryclose branch' on goal 314 (script from line 81) 
720125     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 30: 'rule exLeft' on goal 315 (script from line 82) 
720127     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 31: 'rule andLeft' on goal 420 (script from line 83) 
720128     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 32: 'rule andLeft' on goal 421 (script from line 84) 
720129     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 33: 'instantiate var=iv with='jv_0' occ=1' on goal 422 (script from line 86) 
720130     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 34: 'rule impLeft' on goal 423 (script from line 87) 
720131     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 35: 'tryclose branch' on goal 424 (script from line 88) 
720139     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 36: 'rule andLeft' on goal 425 (script from line 89) 
720140     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 37: 'rule andLeft' on goal 434 (script from line 90) 
720142     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 38: 'rule castAdd formula='s_0[jv_0] = v_x_0' occ=0' on goal 435 (script from line 91) 
720143     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 39: 'instantiate hide var=iv with='jv_1' occ=1' on goal 436 (script from line 93) 
720143     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 40: 'rule impLeft' on goal 437 (script from line 94) 
720145     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 41: 'tryclose branch' on goal 438 (script from line 95) 
720152     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 42: 'rule andLeft' on goal 439 (script from line 96) 
720153     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 43: 'rule andLeft' on goal 448 (script from line 97) 
720154     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 44: 'rule castAdd formula='s_0[jv_1] = v_y_0' occ=0' on goal 449 (script from line 98) 
720155     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 45: 'instantiate var=iv  with='v_x_0'' on goal 450 (script from line 100) 
720156     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 46: 'rule impLeft' on goal 451 (script from line 101) 
720157     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 47: 'tryclose branch' on goal 452 (script from line 102) 
720315     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 48: 'instantiate var=iv  with='v_y_0'' on goal 453 (script from line 104) 
720316     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 49: 'rule impLeft' on goal 562 (script from line 105) 
720317     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 50: 'tryclose branch' on goal 563 (script from line 106) 
720461     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 51: 'cut 'v_x_0 = v_y_0'' on goal 564 (script from line 108) 
720463     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)'' on goal 674 (script from line 110) 
720464     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 53: 'rule andRight' on goal 676 (script from line 112) 
720466     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 54: 'rule andRight' on goal 677 (script from line 113) 
720467     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 55: 'rule andRight' on goal 679 (script from line 114) 
720468     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 56: 'rule andRight' on goal 681 (script from line 115) 
720469     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 57: 'rule lenOfSwap' on goal 683 (script from line 116) 
720470     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 58: 'tryclose branch' on goal 685 (script from line 117) 
720474     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 59: 'rule seqNPermSwapNPerm' on goal 684 (script from line 119) 
720475     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 60: 'instantiate hide var='iv' with='v_x_0' occ=1' on goal 687 (script from line 120) 
720476     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 61: 'instantiate hide var='jv' with='jv_0'' on goal 688 (script from line 121) 
720478     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 62: 'rule impLeft' on goal 689 (script from line 122) 
720479     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 63: 'tryclose branch' on goal 690 (script from line 123) 
720606     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 64: 'tryclose branch' on goal 691 (script from line 124) 
720611     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 65: 'rule allRight' on goal 682 (script from line 126) 
720612     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 66: 'rule impRight' on goal 796 (script from line 127) 
720614     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 67: 'rule andLeft' on goal 797 (script from line 128) 
720615     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 68: 'instantiate var=iv with='v_iv_0'' on goal 798 (script from line 129) 
720615     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 69: 'rule impLeft' on goal 799 (script from line 130) 
720616     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 70: 'tryclose branch' on goal 800 (script from line 131) 
720766     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 71: 'rule getOfSwap' on goal 801 (script from line 132) 
720767     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 72: 'rule ifthenelse_negated' on goal 912 (script from line 133) 
720769     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 73: 'rule ifthenelse_split occ=0' on goal 913 (script from line 134) 
720770     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 74: 'rule andLeft' on goal 914 (script from line 135) 
720771     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 75: 'rule andLeft' on goal 916 (script from line 136) 
720772     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 76: 'rule andLeft' on goal 917 (script from line 137) 
720773     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 77: 'rule ifthenelse_split occ=0' on goal 918 (script from line 138) 
720773     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 78: 'tryclose branch' on goal 919 (script from line 139) 
720935     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 79: 'rule ifthenelse_split occ=0' on goal 920 (script from line 140) 
720936     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 80: 'tryclose branch' on goal 1011 (script from line 141) 
721059     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 81: 'tryclose branch' on goal 1012 (script from line 142) 
721064     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 82: 'tryclose branch' on goal 915 (script from line 143) 
721069     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 83: 'rule getOfSwap' on goal 680 (script from line 145) 
721070     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 84: 'rule ifthenelse_negated' on goal 1099 (script from line 146) 
721071     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 85: 'rule ifthenelse_split occ=0' on goal 1100 (script from line 147) 
721072     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 86: 'rule andLeft' on goal 1101 (script from line 148) 
721073     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 87: 'rule andLeft' on goal 1103 (script from line 149) 
721073     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 88: 'rule andLeft' on goal 1104 (script from line 150) 
721074     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 89: 'rule ifthenelse_split occ=0' on goal 1105 (script from line 151) 
721075     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 90: 'tryclose branch' on goal 1106 (script from line 152) 
721084     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 91: 'tryclose branch' on goal 1107 (script from line 153) 
721090     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 92: 'tryclose branch' on goal 1102 (script from line 154) 
721207     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 93: 'rule getOfSwap' on goal 678 (script from line 156) 
721208     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 94: 'rule ifthenelse_negated' on goal 1225 (script from line 157) 
721209     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 95: 'rule ifthenelse_split occ=0' on goal 1226 (script from line 158) 
721210     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 96: 'rule andLeft' on goal 1227 (script from line 159) 
721211     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 97: 'rule andLeft' on goal 1229 (script from line 160) 
721212     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 98: 'rule andLeft' on goal 1230 (script from line 161) 
721212     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 99: 'rule ifthenelse_split occ=0' on goal 1231 (script from line 162) 
721213     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 100: 'tryclose branch' on goal 1232 (script from line 163) 
721274     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 101: 'tryclose branch' on goal 1233 (script from line 164) 
721281     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 102: 'tryclose branch' on goal 1228 (script from line 165) 
721394     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 103: 'cut '(int)s_0[v_x_0] = (int)s_0[v_y_0]'' on goal 675 (script from line 168) 
721395     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 104: 'rule seqNPermInjective' on goal 1397 (script from line 169) 
721396     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 105: 'instantiate hide var=iv with='v_x_0'' on goal 1399 (script from line 170) 
721397     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 106: 'instantiate hide var=jv with='v_y_0'' on goal 1400 (script from line 171) 
721398     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 107: 'rule impLeft' on goal 1401 (script from line 172) 
721399     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 108: 'tryclose branch' on goal 1402 (script from line 173) 
721563     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 109: 'tryclose branch' on goal 1403 (script from line 174) 
721568     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 110: 'cut '(int)s_0[v_x_0] = v_x_0'' on goal 1398 (script from line 176) 
721569     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)'' on goal 1534 (script from line 178) 
721570     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 112: 'rule andRight' on goal 1536 (script from line 180) 
721572     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 113: 'rule andRight' on goal 1537 (script from line 181) 
721572     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 114: 'rule andRight' on goal 1539 (script from line 182) 
721573     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 115: 'rule andRight' on goal 1541 (script from line 183) 
721574     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 116: 'tryclose branch' on goal 1543 (script from line 184) 
721587     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 117: 'rule seqNPermSwapNPerm' on goal 1544 (script from line 186) 
721588     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 118: 'instantiate hide var=iv with='v_y_0'' on goal 1558 (script from line 187) 
721589     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 119: 'instantiate hide var=jv with='jv_1'' on goal 1559 (script from line 188) 
721590     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 120: 'tryclose branch' on goal 1560 (script from line 189) 
721749     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 121: 'rule allRight' on goal 1542 (script from line 191) 
721750     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 122: 'rule impRight' on goal 1667 (script from line 192) 
721751     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 123: 'rule andLeft' on goal 1668 (script from line 193) 
721752     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 124: 'instantiate var=iv with='v_iv_0'' on goal 1669 (script from line 194) 
721752     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 125: 'rule impLeft' on goal 1670 (script from line 195) 
721753     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 126: 'tryclose branch' on goal 1671 (script from line 196) 
721912     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 127: 'rule getOfSwap' on goal 1672 (script from line 197) 
721913     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 128: 'rule ifthenelse_negated' on goal 1786 (script from line 198) 
721914     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 129: 'rule ifthenelse_split occ=0' on goal 1787 (script from line 199) 
721916     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 130: 'rule andLeft' on goal 1788 (script from line 200) 
721917     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 131: 'rule andLeft' on goal 1790 (script from line 201) 
721917     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 132: 'rule andLeft' on goal 1791 (script from line 202) 
721918     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 133: 'rule ifthenelse_split occ=0' on goal 1792 (script from line 203) 
721919     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 134: 'tryclose branch' on goal 1793 (script from line 204) 
722040     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 135: 'rule ifthenelse_split occ=0' on goal 1794 (script from line 205) 
722042     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 136: 'tryclose branch' on goal 1885 (script from line 206) 
722152     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 137: 'instantiate var=iv with='v_y_0'' on goal 1886 (script from line 207) 
722153     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 138: 'rule impLeft' on goal 1968 (script from line 208) 
722153     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 139: 'tryclose branch' on goal 1969 (script from line 209) 
722159     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 140: 'tryclose branch' on goal 1970 (script from line 210) 
722164     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 141: 'tryclose branch' on goal 1789 (script from line 211) 
722169     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 142: 'tryclose branch' on goal 1540 (script from line 212) 
722327     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 143: 'rule getOfSwap' on goal 1538 (script from line 214) 
722328     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 144: 'rule ifthenelse_negated' on goal 2097 (script from line 215) 
722329     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 145: 'rule ifthenelse_split occ=0' on goal 2098 (script from line 216) 
722330     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 146: 'tryclose branch' on goal 2099 (script from line 217) 
722343     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 147: 'tryclose branch' on goal 2100 (script from line 218) 
722449     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 148: 'tryclose branch' on goal 1535 (script from line 220) 
726907     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 149: 'cut  '(int)s_0[v_y_0] = v_y_0'' on goal 1535 (script from line 223) 
726908     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)'' on goal 4266 (script from line 225) 
726912     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 151: 'rule andRight' on goal 4268 (script from line 227) 
726913     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 152: 'rule andRight' on goal 4269 (script from line 228) 
726914     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 153: 'rule andRight' on goal 4271 (script from line 229) 
726914     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 154: 'rule andRight' on goal 4273 (script from line 230) 
726915     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 155: 'tryclose branch' on goal 4275 (script from line 231) 
726924     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 156: 'rule seqNPermSwapNPerm' on goal 4276 (script from line 233) 
726924     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 157: 'instantiate hide var=iv with='v_x_0'' on goal 4287 (script from line 234) 
726925     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 158: 'instantiate hide var=jv with='jv_0'' on goal 4288 (script from line 235) 
726926     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 159: 'rule impLeft' on goal 4289 (script from line 236) 
726927     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 160: 'tryclose branch' on goal 4290 (script from line 237) 
727033     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 161: 'tryclose branch' on goal 4291 (script from line 238) 
727038     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 162: 'rule allRight' on goal 4274 (script from line 240) 
727038     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 163: 'rule impRight' on goal 4400 (script from line 241) 
727039     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 164: 'rule andLeft' on goal 4401 (script from line 242) 
727040     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 165: 'instantiate var=iv with='v_iv_0'' on goal 4402 (script from line 243) 
727040     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 166: 'rule impLeft' on goal 4403 (script from line 244) 
727041     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 167: 'tryclose branch' on goal 4404 (script from line 245) 
727149     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 168: 'rule getOfSwap' on goal 4405 (script from line 246) 
727150     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 169: 'rule ifthenelse_negated' on goal 4521 (script from line 247) 
727151     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 170: 'rule ifthenelse_split occ=0' on goal 4522 (script from line 248) 
727152     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 171: 'rule andLeft' on goal 4523 (script from line 249) 
727153     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 172: 'rule andLeft' on goal 4525 (script from line 250) 
727153     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 173: 'rule andLeft' on goal 4526 (script from line 251) 
727154     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 174: 'rule ifthenelse_split occ=0' on goal 4527 (script from line 252) 
727154     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 175: 'tryclose branch' on goal 4528 (script from line 253) 
727242     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 176: 'rule ifthenelse_split occ=0' on goal 4529 (script from line 254) 
727243     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 177: 'tryclose branch' on goal 4622 (script from line 255) 
727329     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 178: 'tryclose branch' on goal 4623 (script from line 256) 
727334     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 179: 'tryclose branch' on goal 4524 (script from line 257) 
727339     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 180: 'rule getOfSwap' on goal 4272 (script from line 259) 
727339     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 181: 'rule ifthenelse_negated' on goal 4713 (script from line 260) 
727340     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 182: 'rule ifthenelse_split occ=0' on goal 4714 (script from line 261) 
727341     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 183: 'tryclose branch' on goal 4715 (script from line 262) 
727352     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 184: 'tryclose branch' on goal 4716 (script from line 263) 
727445     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 185: 'rule getOfSwap' on goal 4270 (script from line 265) 
727446     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 186: 'rule ifthenelse_negated' on goal 4839 (script from line 266) 
727447     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 187: 'rule ifthenelse_split occ=0' on goal 4840 (script from line 267) 
727448     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 188: 'tryclose branch' on goal 4841 (script from line 268) 
727527     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 189: 'tryclose branch' on goal 4842 (script from line 269) 
727538     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 190: 'cut '(int)s_0[v_x_0]=v_y_0'' on goal 4267 (script from line 272) 
727539     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)'' on goal 4948 (script from line 274) 
727539     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 192: 'rule andRight' on goal 4950 (script from line 276) 
727541     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 193: 'rule andRight' on goal 4951 (script from line 277) 
727541     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 194: 'rule andRight' on goal 4953 (script from line 278) 
727542     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 195: 'rule andRight' on goal 4955 (script from line 279) 
727542     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 196: 'tryclose branch' on goal 4957 (script from line 280) 
727554     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 197: 'rule seqNPermSwapNPerm' on goal 4958 (script from line 282) 
727554     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 198: 'instantiate hide var=iv with='jv_0'' on goal 4977 (script from line 283) 
727555     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 199: 'instantiate hide var=jv with='v_x_0'' on goal 4978 (script from line 284) 
727556     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 200: 'rule impLeft' on goal 4979 (script from line 285) 
727557     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 201: 'tryclose branch' on goal 4980 (script from line 286) 
727653     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 202: 'rule seqNPermSwapNPerm formula='seqNPerm(seqSwap(s_0, jv_0, v_x_0))'' on goal 4981 (script from line 287) 
727654     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 203: 'instantiate hide var=iv with='jv_0'' on goal 5093 (script from line 288) 
727655     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 204: 'instantiate hide var=jv with='v_y_0'' on goal 5094 (script from line 289) 
727656     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 205: 'rule impLeft' on goal 5095 (script from line 290) 
727656     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 206: 'tryclose branch' on goal 5096 (script from line 291) 
727756     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 207: 'tryclose branch' on goal 5097 (script from line 292) 
727760     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 208: 'rule allRight' on goal 4956 (script from line 294) 
727761     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 209: 'rule impRight' on goal 5212 (script from line 295) 
727762     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 210: 'rule andLeft' on goal 5213 (script from line 296) 
727762     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 211: 'instantiate var=iv with='v_iv_0'' on goal 5214 (script from line 299) 
727763     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 212: 'rule impLeft' on goal 5215 (script from line 300) 
727763     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 213: 'tryclose branch' on goal 5216 (script from line 301) 
727876     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 214: 'rule getOfSwap' on goal 5217 (script from line 303) 
727878     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 215: 'rule ifthenelse_negated' on goal 5337 (script from line 304) 
727879     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 216: 'rule ifthenelse_split occ=0' on goal 5338 (script from line 305) 
727880     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 217: 'rule andLeft' on goal 5339 (script from line 306) 
727882     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 218: 'rule andLeft' on goal 5341 (script from line 307) 
727884     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 219: 'rule andLeft' on goal 5342 (script from line 308) 
727886     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 220: 'rule ifthenelse_split occ=0' on goal 5343 (script from line 309) 
727888     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 221: 'rule getOfSwap' on goal 5344 (script from line 310) 
727889     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 222: 'rule ifthenelse_negated' on goal 5346 (script from line 311) 
727890     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 223: 'rule ifthenelse_split occ=0' on goal 5347 (script from line 312) 
727891     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 224: 'rule andLeft' on goal 5348 (script from line 313) 
727892     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 225: 'rule andLeft' on goal 5350 (script from line 314) 
727893     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 226: 'rule andLeft' on goal 5351 (script from line 315) 
727893     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 227: 'rule ifthenelse_split occ=0' on goal 5352 (script from line 316) 
727894     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 228: 'tryclose branch' on goal 5353 (script from line 317) 
727992     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 229: 'rule ifthenelse_split occ=0' on goal 5354 (script from line 318) 
727994     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 230: 'tryclose branch' on goal 5463 (script from line 319) 
728001     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 231: 'tryclose branch' on goal 5464 (script from line 320) 
728087     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 232: 'tryclose branch' on goal 5349 (script from line 321) 
728176     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 233: 'rule ifthenelse_split' on goal 5345 (script from line 323) 
728177     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 234: 'rule getOfSwap' on goal 5660 (script from line 324) 
728178     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 235: 'rule ifthenelse_negated' on goal 5662 (script from line 325) 
728179     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 236: 'rule ifthenelse_split occ=0' on goal 5663 (script from line 326) 
728180     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 237: 'rule andLeft' on goal 5664 (script from line 327) 
728180     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 238: 'rule andLeft' on goal 5666 (script from line 328) 
728181     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 239: 'rule andLeft' on goal 5667 (script from line 329) 
728181     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 240: 'rule ifthenelse_split occ=0' on goal 5668 (script from line 330) 
728182     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 241: 'tryclose branch' on goal 5669 (script from line 331) 
728277     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 242: 'tryclose branch' on goal 5670 (script from line 332) 
728286     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 243: 'tryclose branch' on goal 5665 (script from line 333) 
728391     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 244: 'rule getOfSwap' on goal 5661 (script from line 335) 
728392     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 245: 'rule ifthenelse_negated' on goal 5887 (script from line 336) 
728393     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 246: 'rule ifthenelse_split occ=0' on goal 5888 (script from line 337) 
728394     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 247: 'rule andLeft' on goal 5889 (script from line 338) 
728395     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 248: 'rule andLeft' on goal 5891 (script from line 339) 
728395     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 249: 'rule andLeft' on goal 5892 (script from line 340) 
728396     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 250: 'rule ifthenelse_split occ=0' on goal 5893 (script from line 341) 
728396     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 251: 'tryclose branch' on goal 5894 (script from line 342) 
728402     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 252: 'rule ifthenelse_split occ=0' on goal 5895 (script from line 343) 
728403     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 253: 'tryclose branch' on goal 5897 (script from line 344) 
728492     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 254: 'tryclose branch' on goal 5898 (script from line 345) 
728498     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 255: 'tryclose branch' on goal 5890 (script from line 346) 
728511     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 256: 'tryclose branch' on goal 5340 (script from line 347) 
728624     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 257: 'rule getOfSwap' on goal 4954 (script from line 349) 
728625     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 258: 'rule ifthenelse_negated' on goal 6115 (script from line 350) 
728626     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 259: 'rule ifthenelse_split occ=0' on goal 6116 (script from line 351) 
728627     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 260: 'rule andLeft' on goal 6117 (script from line 352) 
728628     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 261: 'rule andLeft' on goal 6119 (script from line 353) 
728629     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 262: 'rule andLeft' on goal 6120 (script from line 354) 
728630     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 263: 'rule ifthenelse_split occ=0' on goal 6121 (script from line 355) 
728630     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 264: 'tryclose branch' on goal 6122 (script from line 356) 
728691     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 265: 'rule ifthenelse_split occ=0' on goal 6123 (script from line 357) 
728692     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 266: 'rule getOfSwap' on goal 6193 (script from line 358) 
728692     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 267: 'rule ifthenelse_negated' on goal 6195 (script from line 359) 
728693     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 268: 'rule ifthenelse_split occ=0' on goal 6196 (script from line 360) 
728694     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 269: 'tryclose branch' on goal 6197 (script from line 361) 
728701     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 270: 'tryclose branch' on goal 6198 (script from line 362) 
728707     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 271: 'tryclose branch' on goal 6194 (script from line 363) 
728841     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 272: 'tryclose branch' on goal 6118 (script from line 364) 
728987     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 273: 'rule getOfSwap' on goal 4952 (script from line 366) 
728988     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 274: 'rule ifthenelse_negated' on goal 6456 (script from line 367) 
728989     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 275: 'rule ifthenelse_split occ=0' on goal 6457 (script from line 368) 
728990     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 276: 'tryclose branch' on goal 6458 (script from line 369) 
729182     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 277: 'tryclose branch' on goal 6459 (script from line 370) 
729283     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 278: 'cut 'int::seqGet(s_0, v_y_0)=v_x_0'' on goal 4949 (script from line 374) 
729283     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 279: 'tryclose branch' on goal 6735 (script from line 377) 
732957     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 280: 'rule seqNPermSwapNPerm' on goal 6735 (script from line 379) 
732962     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 281: 'instantiate hide var=iv with='jv_1'' on goal 8783 (script from line 380) 
732963     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 282: 'instantiate hide var=jv with='v_y_0'' on goal 8784 (script from line 381) 
732964     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 283: 'rule impLeft' on goal 8785 (script from line 382) 
732964     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 284: 'tryclose branch' on goal 8786 (script from line 383) 
733099     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 285: 'rule seqNPermSwapNPerm formula='seqNPerm(seqSwap(s_0,jv_1,v_y_0))'' on goal 8787 (script from line 384) 
733099     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 286: 'instantiate hide var=iv with='jv_1'' on goal 8909 (script from line 385) 
733100     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 287: 'instantiate hide var=jv with='v_x_0'' on goal 8910 (script from line 386) 
733101     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 288: 'rule impLeft' on goal 8911 (script from line 387) 
733102     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 289: 'tryclose branch' on goal 8912 (script from line 388) 
733229     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 290: 'tryclose branch' on goal 8913 (script from line 389) 
736874     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 291: 'tryclose branch' on goal 6736 (script from line 396) 
740578     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 292: 'rule seqNPermSwapNPerm formula='seqNPerm(s_0)'' on goal 6736 (script from line 398) 
740582     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 293: 'instantiate hide var=iv with='v_x_0'' on goal 12633 (script from line 399) 
740583     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 294: 'instantiate hide var=jv with='jv_0'' on goal 12634 (script from line 400) 
740583     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 295: 'rule impLeft' on goal 12635 (script from line 401) 
740584     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 296: 'tryclose branch' on goal 12636 (script from line 402) 
740704     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 297: 'rule seqNPermSwapNPerm formula='seqNPerm(seqSwap(s_0,v_x_0,jv_0))'' on goal 12637 (script from line 403) 
740704     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 298: 'instantiate hide var=iv with='v_y_0'' on goal 12757 (script from line 404) 
740705     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 299: 'instantiate hide var=jv with='jv_1'' on goal 12758 (script from line 405) 
740707     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)' ...' on goal 12759 (script from line 406) 
740707     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 301: 'tryclose branch' on goal 12760 (script from line 407) 
741950     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm2/Taclet_schiffl_thm_1.proof 
741950     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 81.91ns 
741951     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
744702     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.75s 
744703     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: schiffl_thm_1 
745554     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: schiffl_thm_1 
745556     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 19.6ns 
745556     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 1: 'macro split-prop' on goal 0 (script from line 50) 
745565     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 2: 'rule schiffl_lemma_2 formula='seqPerm(f_s, f_t)'' on goal 10 (script from line 51) 
745575     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 3: 'instantiate hide var=x with='f_x'' on goal 11 (script from line 52) 
745577     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 4: 'instantiate hide var=y with='f_y'' on goal 12 (script from line 53) 
745579     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 5: 'rule impLeft' on goal 13 (script from line 54) 
745581     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 6: 'tryclose branch' on goal 14 (script from line 55) 
745586     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 7: 'rule exLeft' on goal 15 (script from line 56) 
745586     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 8: 'macro split-prop' on goal 23 (script from line 57) 
745640     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 9: 'rule seqPermDef occ=1' on goal 27 (script from line 58) 
745641     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 10: 'rule andRight' on goal 28 (script from line 59) 
745643     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 11: 'tryclose branch' on goal 29 (script from line 60) 
745654     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 12: 'instantiate hide var=s with='r_0'' on goal 30 (script from line 61) 
745654     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 13: 'rule andRight' on goal 46 (script from line 62) 
745656     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 14: 'tryclose branch' on goal 47 (script from line 63) 
745709     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 15: 'rule allRight' on goal 48 (script from line 64) 
745710     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 16: 'rule impRight' on goal 119 (script from line 65) 
745711     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 17: 'instantiate hide var=iv with='iv_0'' on goal 120 (script from line 66) 
745711     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 18: 'rule impLeft' on goal 121 (script from line 67) 
745712     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 19: 'tryclose branch' on goal 122 (script from line 68) 
745782     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 20: 'rule andLeft' on goal 123 (script from line 69) 
745783     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 21: 'rule seqNPermRange' on goal 203 (script from line 70) 
745783     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 22: 'instantiate hide var=iv with='iv_0'' on goal 204 (script from line 71) 
745784     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 23: 'rule impLeft' on goal 205 (script from line 72) 
745785     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 24: 'tryclose branch' on goal 206 (script from line 73) 
745789     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 25: 'rule andLeft' on goal 207 (script from line 74) 
745789     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 26: 'rule andLeft' on goal 215 (script from line 75) 
745790     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 27: 'rule seqNPermRange' on goal 216 (script from line 76) 
745790     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 28: 'instantiate hide var=iv with='f_x'' on goal 217 (script from line 77) 
745791     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 29: 'rule impLeft' on goal 218 (script from line 78) 
745792     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 30: 'tryclose branch' on goal 219 (script from line 79) 
745883     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 31: 'rule andLeft' on goal 220 (script from line 80) 
745884     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 32: 'rule andLeft' on goal 311 (script from line 81) 
745884     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 33: 'rule seqNPermRange' on goal 312 (script from line 82) 
745885     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 34: 'instantiate hide var=iv with='f_y'' on goal 313 (script from line 83) 
745886     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 35: 'rule impLeft' on goal 314 (script from line 84) 
745887     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 36: 'tryclose branch' on goal 315 (script from line 85) 
745981     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 37: 'rule andLeft' on goal 316 (script from line 86) 
745982     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 38: 'rule andLeft' on goal 410 (script from line 87) 
745982     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 39: 'rule getOfSeqDef occ=0' on goal 411 (script from line 88) 
745983     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 40: 'rule getOfSeqDef' on goal 412 (script from line 89) 
745983     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 41: 'rule ifthenelse_split occ=0' on goal 413 (script from line 90) 
745984     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 42: 'rule andLeft occ=0' on goal 414 (script from line 91) 
745985     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 43: 'rule sub_zero_2 occ=0' on goal 416 (script from line 92) 
745985     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 44: 'rule ifthenelse_split occ=2' on goal 417 (script from line 93) 
745986     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 45: 'rule andLeft' on goal 418 (script from line 94) 
745987     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 46: 'rule sub_zero_2 occ=0' on goal 420 (script from line 95) 
745987     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 47: 'rule add_zero_right occ=0' on goal 421 (script from line 96) 
745988     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 48: 'rule add_zero_right occ=0' on goal 422 (script from line 97) 
745988     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 49: 'rule add_zero_right occ=0' on goal 423 (script from line 98) 
745989     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 50: 'rule add_zero_right occ=0' on goal 424 (script from line 99) 
745989     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 51: 'rule add_zero_right occ=0' on goal 425 (script from line 100) 
745990     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 52: 'rule add_zero_right occ=0' on goal 426 (script from line 101) 
745990     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 53: 'rule ifthenelse_split occ=0' on goal 427 (script from line 102) 
745991     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 54: 'rule ifthenelse_split occ=0' on goal 428 (script from line 103) 
745992     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 55: 'tryclose branch' on goal 430 (script from line 104) 
745994     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 56: 'tryclose branch' on goal 431 (script from line 105) 
746035     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 57: 'rule ifthenelse_split occ=0' on goal 429 (script from line 106) 
746036     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 58: 'tryclose branch' on goal 473 (script from line 107) 
746099     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 59: 'rule ifthenelse_split occ=0' on goal 474 (script from line 108) 
746100     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 60: 'rule seqNPermInjective' on goal 541 (script from line 109) 
746101     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 61: 'instantiate hide var=iv with='iv_0'' on goal 543 (script from line 110) 
746102     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 62: 'instantiate hide var=jv with='f_y'' on goal 544 (script from line 111) 
746103     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 63: 'rule impLeft' on goal 545 (script from line 112) 
746104     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 64: 'tryclose branch' on goal 546 (script from line 113) 
746176     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 65: 'tryclose branch' on goal 547 (script from line 114) 
746184     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 66: 'rule ifthenelse_split occ=0' on goal 542 (script from line 115) 
746186     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 67: 'rule seqNPermInjective' on goal 606 (script from line 116) 
746189     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 68: 'instantiate hide var=iv with='iv_0'' on goal 608 (script from line 117) 
746193     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 69: 'instantiate hide var=jv with='f_x'' on goal 609 (script from line 118) 
746196     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 70: 'rule impLeft' on goal 610 (script from line 119) 
746198     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 71: 'tryclose branch' on goal 611 (script from line 120) 
746248     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 72: 'tryclose branch' on goal 612 (script from line 121) 
746252     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 73: 'tryclose branch' on goal 607 (script from line 122) 
746255     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 74: 'tryclose branch' on goal 419 (script from line 123) 
746312     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 75: 'tryclose branch' on goal 415 (script from line 124) 
746372     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_eqSameSeq.proof 
746372     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 286.81ns 
746373     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
749023     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.65s 
749023     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: eqSameSeq 
749914     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: eqSameSeq 
749931     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 13.66ms