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

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

tests
0

failures
0

ignored
12m44.68s

duration
100%

successful

Tests

Test Method name Duration Result
powPositive data()[100] 3.611s passed
powPositiveConcrete data()[101] 3.675s passed
powGeq1Concrete data()[102] 3.807s passed
pow2InIntLower data()[103] 3.690s passed
pow2InIntUpper data()[104] 3.671s passed
logSelfConcrete data()[105] 3.681s passed
log1Concrete data()[106] 3.631s passed
logProduct data()[107] 3.719s passed
logTimesBaseConcrete data()[108] 3.634s passed
logProdIdentity data()[109] 3.661s passed
moduloByteIsInByte data()[10] 3.904s passed
logProdIdentityConcrete data()[110] 3.738s passed
logPowIdentity data()[111] 3.615s passed
logPowIdentityConcrete data()[112] 3.681s passed
logPositive data()[113] 3.729s passed
logPositiveConcrete data()[114] 3.746s passed
logMono data()[115] 3.744s passed
logMonoConcrete data()[116] 3.655s passed
powLogLess data()[117] 3.660s passed
powLogMore2 data()[118] 3.713s passed
logLessThanPow data()[119] 3.629s passed
moduloCharIsInChar data()[11] 3.717s passed
logLessThanPowConcrete data()[120] 3.624s passed
logSqueeze data()[121] 3.822s passed
ifthenelse_equals data()[122] 3.668s passed
ifthenelse_equals_1 data()[123] 3.738s passed
ifthenelse_equals_2 data()[124] 3.683s passed
disjointWithSingleton1 data()[125] 3.748s passed
disjointWithSingleton2 data()[126] 3.661s passed
disjointArrayRanges data()[127] 3.589s passed
disjointArrayRangeAllFields1 data()[128] 3.649s passed
disjointArrayRangeAllFields2 data()[129] 3.677s passed
div_unique1 data()[12] 3.918s passed
seqSelfDefinition data()[130] 3.927s passed
seqOutsideValue data()[131] 3.812s passed
castedGetAny data()[132] 3.821s passed
seqGetAlphaCast data()[133] 3.693s passed
getOfSeqSingleton data()[134] 3.743s passed
getOfSeqSingletonConcrete data()[135] 3.703s passed
getOfSeqConcat data()[136] 3.683s passed
getOfSeqSub data()[137] 3.680s passed
getOfSeqReverse data()[138] 3.549s passed
lenOfSeqEmpty data()[139] 3.564s passed
div_unique2 data()[13] 3.876s passed
lenOfSeqSingleton data()[140] 3.685s passed
lenOfSeqConcat data()[141] 3.668s passed
lenOfSeqSub data()[142] 3.566s passed
lenOfSeqReverse data()[143] 3.841s passed
equalityToSeqGetAndSeqLenLeft data()[144] 3.680s passed
equalityToSeqGetAndSeqLenRight data()[145] 3.688s passed
getOfSeqSingletonEQ data()[146] 3.714s passed
getOfSeqConcatEQ data()[147] 3.859s passed
getOfSeqSubEQ data()[148] 3.640s passed
getOfSeqReverseEQ data()[149] 3.622s passed
div_exists data()[14] 3.943s passed
lenOfSeqEmptyEQ data()[150] 3.735s passed
lenOfSeqSingletonEQ data()[151] 3.688s passed
lenOfSeqConcatEQ data()[152] 3.632s passed
lenOfSeqSubEQ data()[153] 3.663s passed
lenOfSeqReverseEQ data()[154] 3.658s passed
getOfSeqDefEQ data()[155] 3.681s passed
lenOfSeqDefEQ data()[156] 3.702s passed
seqConcatWithSeqEmpty1 data()[157] 3.649s passed
seqConcatWithSeqEmpty2 data()[158] 3.826s passed
seqReverseOfSeqEmpty data()[159] 3.726s passed
div_one data()[15] 3.824s passed
subSeqComplete data()[160] 3.778s passed
subSeqTailR data()[161] 3.755s passed
subSeqTailL data()[162] 3.698s passed
subSeqTailEQR data()[163] 3.638s passed
subSeqTailEQL data()[164] 3.726s passed
seqDef_split data()[165] 3.793s passed
seqDef_induction_upper data()[166] 3.828s passed
seqDef_induction_upper_concrete data()[167] 3.849s passed
seqDef_induction_lower data()[168] 3.754s passed
seqDef_induction_lower_concrete data()[169] 3.825s passed
jdiv_one data()[16] 3.712s passed
seqDef_split_in_three data()[170] 3.826s passed
seqDef_empty data()[171] 3.820s passed
seqDef_one_summand data()[172] 3.794s passed
seqDef_lower_equals_upper data()[173] 3.862s passed
seqDefOfSeq data()[174] 3.831s passed
seqSelfDefinitionEQ2 data()[175] 3.906s passed
indexOfSeqSingleton data()[176] 3.926s passed
indexOfSeqConcatFirst data()[177] 3.817s passed
indexOfSeqConcatSecond data()[178] 3.793s passed
indexOfSeqSub data()[179] 3.784s passed
div_zero data()[17] 3.800s passed
lenOfArray2seq data()[180] 3.798s passed
getAnyOfArray2seq data()[181] 3.892s passed
getOfArray2seq data()[182] 3.806s passed
getAnyOfNPermInv data()[183] 3.819s passed
seqNPermRange data()[184] 3.872s passed
seqPermTrans data()[185] 3.821s passed
seqPermRefl data()[186] 3.786s passed
seqPermSplit data()[187] 3.753s passed
seqNPermRight data()[188] 3.852s passed
seqPermFromSwap data()[189] 3.683s passed
divResZero1 data()[18] 3.823s passed
seqPermTransAlt0 data()[190] 3.794s passed
seqPermTransAlt1 data()[191] 3.658s passed
seqPermTransAlt2 data()[192] 3.759s passed
seqPermTransAlt3 data()[193] 3.747s passed
seqPermForall data()[194] 3.754s passed
seqPermExists data()[195] 3.740s passed
schiffl_lemma_2 data()[196] 25.404s passed
schiffl_thm_1 data()[197] 4.563s passed
eqSameSeq data()[198] 4.066s passed
divResZero2 data()[19] 3.747s passed
eqTermCut data()[1] 4.654s passed
divResOne1 data()[20] 3.757s passed
divResOne2 data()[21] 3.736s passed
div_cancel1 data()[22] 3.825s passed
div_cancel2 data()[23] 3.797s passed
divAddMultDenom data()[24] 3.885s passed
divMinus data()[25] 3.886s passed
divMinusDenom data()[26] 3.808s passed
divLeastDPos data()[27] 3.809s passed
divLeastDNeg data()[28] 3.777s passed
divGreatestDPos data()[29] 3.814s passed
equivAllRight data()[2] 4.305s passed
divGreatestDNeg data()[30] 3.858s passed
divIncreasingPos data()[31] 3.896s passed
divIncreasingNeg data()[32] 3.811s passed
jdiv_zero data()[33] 3.756s passed
jdivPulloutMinusNum data()[34] 3.681s passed
jdivPulloutMinusDenom data()[35] 3.821s passed
jdiv_uniquePosPos data()[36] 3.927s passed
jdiv_uniquePosNeg data()[37] 3.817s passed
jdiv_uniqueNegPos data()[38] 3.754s passed
jdiv_uniqueNegNeg data()[39] 3.733s passed
irrflConcrete1 data()[3] 4.216s passed
jdivMultDenom1 data()[40] 3.828s passed
jdivMultDenom2 data()[41] 3.849s passed
mod_geZero data()[42] 3.767s passed
mod_lessDenom data()[43] 3.862s passed
jmod_NumPos data()[44] 3.832s passed
jmod_NumNeg data()[45] 3.773s passed
jmod_geZero data()[46] 3.766s passed
jmodNumZero data()[47] 3.695s passed
jmod_pulloutminusNum data()[48] 3.757s passed
jmod_pulloutminusDenom data()[49] 3.672s passed
irrflConcrete2 data()[4] 4.102s passed
jmodUnique1 data()[50] 3.781s passed
jmodUnique2 data()[51] 3.775s passed
intDivRem data()[52] 3.719s passed
jmodjmod data()[53] 3.738s passed
jmodDivisible data()[54] 3.718s passed
jmodDivisibleRep data()[55] 3.647s passed
jdivAddMultDenom data()[56] 3.863s passed
jmodAltZero data()[57] 3.710s passed
jmodAddMultDenomZero data()[58] 3.710s passed
polyDiv_zero data()[59] 3.654s passed
cancel_gtPos data()[5] 4.033s passed
polyMod_ltdivDenom data()[60] 3.657s passed
bsum_empty data()[61] 3.609s passed
bsum_induction_upper data()[62] 3.516s passed
bsum_induction_lower data()[63] 3.582s passed
bsum_num_of_bounds data()[64] 3.629s passed
bsum_num_of_bounds2 data()[65] 3.651s passed
bsum_induction_upper2 data()[66] 3.649s passed
bsum_induction_upper_concrete data()[67] 3.676s passed
bsum_induction_upper_concrete_2 data()[68] 3.660s passed
bsum_induction_upper2_concrete data()[69] 3.649s passed
cancel_gtNeg data()[6] 3.956s passed
bsum_induction_lower_concrete data()[70] 3.569s passed
bsum_induction_lower2 data()[71] 3.650s passed
bsum_induction_lower2_concrete data()[72] 3.661s passed
bsum_positive data()[73] 3.729s passed
bsum_upper_bound data()[74] 3.648s passed
bsum_lower_bound data()[75] 3.665s passed
bsum_positive_lower_bound_element data()[76] 3.730s passed
bsum_sub_same_index data()[77] 3.666s passed
bsum_less_same_index data()[78] 3.621s passed
bsum_equal_except_one_index data()[79] 3.626s passed
moduloIntIsInInt data()[7] 3.917s passed
bsum_num_of_is_max data()[80] 3.656s passed
bsum_num_of_is_max2 data()[81] 3.698s passed
bsum_num_of_is_max3 data()[82] 3.593s passed
bsum_num_of_is_max4 data()[83] 3.652s passed
bsum_num_of_lt_max data()[84] 3.695s passed
bsum_num_of_lt_max2 data()[85] 3.767s passed
bsum_num_of_lt_max3 data()[86] 3.631s passed
bsum_num_of_lt_max4 data()[87] 3.648s passed
bsum_num_of_gt0 data()[88] 3.658s passed
bsum_num_of_gt0_alt data()[89] 3.486s passed
moduloLongIsInLong data()[8] 3.798s passed
bsum_add_concrete data()[90] 3.542s passed
bprod_all_positive data()[91] 3.606s passed
bprod_split data()[92] 3.498s passed
powConcrete0 data()[93] 3.688s passed
powConcrete1 data()[94] 3.903s passed
powSplitFactor data()[95] 3.801s passed
powAdd data()[96] 3.758s passed
powMono data()[97] 3.701s passed
powMonoConcrete data()[98] 3.751s passed
powMonoConcreteRight data()[99] 3.569s passed
moduloShortIsInShort data()[9] 3.813s passed

Standard output

800        INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src/test/resources/testcase/dummyTrue.key 
829        DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 12.31ms 
1044       INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
1070       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)

2138       DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for Meta 
2140       DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for Meta 
2144       DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for Meta 
2144       DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for Meta 
3701       DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for JavaBigintExpression 
10176      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 9.13s 
10244      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof dummyTrue.key 
10283      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 38.7ns 
10298      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/firstOrder/Taclet_eqTermCut.proof 
10299      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 693.4ns 
10304      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
13685      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.38s 
13688      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: eqTermCut 
14908      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: eqTermCut 
14940      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 24.94ms 
14969      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/firstOrder/Taclet_equivAllRight.proof 
14973      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 4.01ms 
14975      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
18173      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.2s 
18174      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: equivAllRight 
19251      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: equivAllRight 
19265      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 10.03ms 
19269      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_irrflConcrete1.proof 
19269      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 160.1ns 
19270      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
22328      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.06s 
22328      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: irrflConcrete1 
23467      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: irrflConcrete1 
23481      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 6ms 
23486      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_irrflConcrete2.proof 
23486      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 150ns 
23487      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
26557      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.07s 
26559      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: irrflConcrete2 
27573      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: irrflConcrete2 
27585      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 7.5ms 
27589      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_cancel_gtPos.proof 
27590      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 949.5ns 
27591      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
30608      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.02s 
30608      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: cancel_gtPos 
31578      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: cancel_gtPos 
31619      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 38.73ms 
31622      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_cancel_gtNeg.proof 
31622      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 170.8ns 
31623      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
34573      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.95s 
34573      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: cancel_gtNeg 
35556      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: cancel_gtNeg 
35576      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 16.05ms 
35578      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intRulesIgnoringOF/Taclet_moduloIntIsInInt.proof 
35578      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 131.6ns 
35579      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
38524      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.95s 
38524      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: moduloIntIsInInt 
39489      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: moduloIntIsInInt 
39493      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 819.2ns 
39495      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intRulesIgnoringOF/Taclet_moduloLongIsInLong.proof 
39495      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 217.4ns 
39497      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
42338      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.84s 
42339      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: moduloLongIsInLong 
43288      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: moduloLongIsInLong 
43291      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 668.9ns 
43293      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intRulesIgnoringOF/Taclet_moduloShortIsInShort.proof 
43294      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 370.3ns 
43295      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
46180      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.89s 
46181      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: moduloShortIsInShort 
47100      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: moduloShortIsInShort 
47103      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 655.9ns 
47107      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intRulesIgnoringOF/Taclet_moduloByteIsInByte.proof 
47107      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 379.3ns 
47108      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
50038      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.93s 
50039      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: moduloByteIsInByte 
51005      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: moduloByteIsInByte 
51008      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 721.3ns 
51012      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intRulesIgnoringOF/Taclet_moduloCharIsInChar.proof 
51012      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 382.5ns 
51013      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
53787      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.77s 
53787      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: moduloCharIsInChar 
54723      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: moduloCharIsInChar 
54726      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 662.7ns 
54729      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_div_unique1.proof 
54730      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 1.18ms 
54737      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
57649      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.91s 
57650      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: div_unique1 
58604      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: div_unique1 
58644      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 36.1ms 
58646      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_div_unique2.proof 
58646      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 184.5ns 
58649      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
61514      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.86s 
61514      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: div_unique2 
62487      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: div_unique2 
62519      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 28.45ms 
62522      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_div_exists.proof 
62523      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 159.5ns 
62524      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
65372      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.85s 
65372      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: div_exists 
66292      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: div_exists 
66462      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 161.43ms 
66466      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_div_one.proof 
66466      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 290.2ns 
66467      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
69352      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.88s 
69352      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: div_one 
70283      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: div_one 
70288      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.59ms 
70290      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdiv_one.proof 
70290      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 108.1ns 
70291      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
73069      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.78s 
73069      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdiv_one 
73997      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdiv_one 
74000      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.11ms 
74003      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_div_zero.proof 
74003      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 303ns 
74005      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
76784      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.78s 
76784      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: div_zero 
77743      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: div_zero 
77799      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 45.42ms 
77804      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divResZero1.proof 
77805      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 415.9ns 
77806      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
80712      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.91s 
80713      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divResZero1 
81611      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divResZero1 
81625      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 9.85ms 
81628      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divResZero2.proof 
81628      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 356.8ns 
81629      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
84426      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.8s 
84427      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divResZero2 
85318      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divResZero2 
85364      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 12.01ms 
85374      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divResOne1.proof 
85374      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 162.3ns 
85375      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
88209      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.83s 
88209      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divResOne1 
89116      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divResOne1 
89129      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 10.16ms 
89132      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divResOne2.proof 
89132      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 369.1ns 
89133      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
91926      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.79s 
91927      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divResOne2 
92853      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divResOne2 
92865      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 9.71ms 
92867      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_div_cancel1.proof 
92867      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 126.9ns 
92868      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
95729      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.86s 
95730      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: div_cancel1 
96671      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: div_cancel1 
96690      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 15.03ms 
96691      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_div_cancel2.proof 
96692      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 129.2ns 
96693      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
99563      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.87s 
99564      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: div_cancel2 
100484     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: div_cancel2 
100488     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.5ms 
100489     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divAddMultDenom.proof 
100489     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 114.9ns 
100490     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
103355     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.87s 
103356     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divAddMultDenom 
104326     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divAddMultDenom 
104372     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 38.23ms 
104374     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divMinus.proof 
104374     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 119.9ns 
104375     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
107251     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.88s 
107252     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divMinus 
108190     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divMinus 
108253     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 56.75ms 
108262     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divMinusDenom.proof 
108262     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 406.8ns 
108263     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
111089     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.83s 
111089     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divMinusDenom 
112031     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divMinusDenom 
112066     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 30.28ms 
112071     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divLeastDPos.proof 
112072     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 1.76ms 
112075     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
114924     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.85s 
114924     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divLeastDPos 
115868     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divLeastDPos 
115876     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 5.26ms 
115879     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divLeastDNeg.proof 
115879     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 362.6ns 
115880     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
118725     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.84s 
118726     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divLeastDNeg 
119636     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divLeastDNeg 
119652     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 13.27ms 
119655     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divGreatestDPos.proof 
119655     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 382.6ns 
119657     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
122510     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.85s 
122510     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divGreatestDPos 
123455     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divGreatestDPos 
123467     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 9.85ms 
123469     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divGreatestDNeg.proof 
123469     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 125ns 
123470     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
126335     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.87s 
126337     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divGreatestDNeg 
127315     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divGreatestDNeg 
127325     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 6.71ms 
127328     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divIncreasingPos.proof 
127329     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 403.3ns 
127330     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
130262     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.93s 
130262     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divIncreasingPos 
131203     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divIncreasingPos 
131221     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 12.77ms 
131228     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divIncreasingNeg.proof 
131229     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 659.8ns 
131230     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
134133     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.9s 
134133     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divIncreasingNeg 
135028     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divIncreasingNeg 
135035     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.78ms 
135038     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdiv_zero.proof 
135038     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 334.3ns 
135039     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
137894     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.85s 
137895     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdiv_zero 
138787     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdiv_zero 
138792     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.5ms 
138794     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdivPulloutMinusNum.proof 
138794     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 327.3ns 
138795     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
141545     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.75s 
141545     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdivPulloutMinusNum 
142463     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdivPulloutMinusNum 
142473     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 7.74ms 
142475     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdivPulloutMinusDenom.proof 
142475     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 116.6ns 
142476     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
145316     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.84s 
145316     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdivPulloutMinusDenom 
146255     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdivPulloutMinusDenom 
146294     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 33.5ms 
146296     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdiv_uniquePosPos.proof 
146296     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 134.6ns 
146297     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
149246     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.95s 
149246     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdiv_uniquePosPos 
150202     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdiv_uniquePosPos 
150221     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 14.68ms 
150223     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdiv_uniquePosNeg.proof 
150224     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 351.2ns 
150225     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
153029     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.8s 
153030     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdiv_uniquePosNeg 
154021     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdiv_uniquePosNeg 
154038     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 13.82ms 
154040     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdiv_uniqueNegPos.proof 
154040     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 128.3ns 
154041     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
156864     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.82s 
156864     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdiv_uniqueNegPos 
157776     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdiv_uniqueNegPos 
157792     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 13.21ms 
157794     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdiv_uniqueNegNeg.proof 
157794     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 121.6ns 
157795     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
160540     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.74s 
160540     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdiv_uniqueNegNeg 
161504     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdiv_uniqueNegNeg 
161525     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 16.98ms 
161527     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdivMultDenom1.proof 
161527     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 110.2ns 
161529     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
164334     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.8s 
164334     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdivMultDenom1 
165315     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdivMultDenom1 
165353     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 31.77ms 
165355     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdivMultDenom2.proof 
165355     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 111.6ns 
165355     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
168251     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.9s 
168252     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdivMultDenom2 
169191     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdivMultDenom2 
169202     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.61ms 
169205     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_mod_geZero.proof 
169205     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 384ns 
169207     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
172051     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.84s 
172051     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: mod_geZero 
172965     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: mod_geZero 
172969     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.06ms 
172971     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_mod_lessDenom.proof 
172971     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 95.6ns 
172972     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
175869     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.9s 
175870     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: mod_lessDenom 
176823     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: mod_lessDenom 
176831     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 5.43ms 
176834     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmod_NumPos.proof 
176834     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 348.7ns 
176835     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
179703     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.87s 
179704     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmod_NumPos 
180654     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmod_NumPos 
180663     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 5.9ms 
180665     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmod_NumNeg.proof 
180666     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 332.3ns 
180667     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
183449     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.78s 
183449     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmod_NumNeg 
184416     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmod_NumNeg 
184436     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 16.65ms 
184438     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmod_geZero.proof 
184438     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 124.3ns 
184438     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
187263     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.82s 
187263     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmod_geZero 
188193     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmod_geZero 
188201     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 5.22ms 
188204     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmodNumZero.proof 
188204     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 90.1ns 
188205     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
190986     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.78s 
190986     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmodNumZero 
191894     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmodNumZero 
191897     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.36ms 
191899     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmod_pulloutminusNum.proof 
191900     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 300.3ns 
191901     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
194748     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.85s 
194749     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmod_pulloutminusNum 
195651     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmod_pulloutminusNum 
195654     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.53ms 
195656     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmod_pulloutminusDenom.proof 
195656     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 134.2ns 
195657     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
198398     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.74s 
198399     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmod_pulloutminusDenom 
199308     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmod_pulloutminusDenom 
199326     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 7.82ms 
199329     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmodUnique1.proof 
199329     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 331.4ns 
199330     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
202060     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.73s 
202060     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmodUnique1 
203027     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmodUnique1 
203107     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 71.76ms 
203111     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmodUnique2.proof 
203111     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 319.9ns 
203112     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
205923     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.81s 
205923     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmodUnique2 
206786     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmodUnique2 
206884     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 83.83ms 
206887     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_intDivRem.proof 
206887     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 323.4ns 
206892     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
209678     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.79s 
209679     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: intDivRem 
210600     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: intDivRem 
210604     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.55ms 
210605     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmodjmod.proof 
210605     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 85.9ns 
210606     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
213367     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.76s 
213367     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmodjmod 
214284     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmodjmod 
214339     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 50.81ms 
214343     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmodDivisible.proof 
214349     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 5.73ms 
214352     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
217095     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.74s 
217095     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmodDivisible 
218036     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmodDivisible 
218059     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 19.86ms 
218061     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmodDivisibleRep.proof 
218061     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 79.6ns 
218062     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
220786     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.72s 
220786     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmodDivisibleRep 
221703     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmodDivisibleRep 
221706     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 864.5ns 
221711     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdivAddMultDenom.proof 
221713     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 1.9ms 
221714     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
224566     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.85s 
224566     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdivAddMultDenom 
225462     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdivAddMultDenom 
225571     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 97.53ms 
225574     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmodAltZero.proof 
225575     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 273.8ns 
225576     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
228349     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.77s 
228349     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmodAltZero 
229271     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmodAltZero 
229282     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 8.55ms 
229284     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmodAddMultDenomZero.proof 
229284     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 71.7ns 
229287     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
232052     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.77s 
232052     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmodAddMultDenomZero 
232986     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmodAddMultDenomZero 
232992     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.75ms 
232994     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_polyDiv_zero.proof 
232994     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 82.9ns 
232995     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
235720     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.73s 
235720     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: polyDiv_zero 
236621     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: polyDiv_zero 
236646     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 22.57ms 
236654     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_polyMod_ltdivDenom.proof 
236654     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 306.5ns 
236655     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
239404     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.75s 
239404     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: polyMod_ltdivDenom 
240292     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: polyMod_ltdivDenom 
240303     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.53ms 
240306     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_empty.proof 
240306     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 72.2ns 
240306     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
243024     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.72s 
243024     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_empty 
243910     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_empty 
243914     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.57ms 
243915     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_induction_upper.proof 
243915     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 76.4ns 
243916     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
246554     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.64s 
246555     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_upper 
247425     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_induction_upper 
247429     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.39ms 
247430     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_induction_lower.proof 
247430     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 63.9ns 
247431     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
250112     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.68s 
250112     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_lower 
250992     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_induction_lower 
251008     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 12.82ms 
251013     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_bounds.proof 
251013     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 72.7ns 
251013     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
253763     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.75s 
253763     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_bounds 
254626     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_bounds 
254640     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 10.93ms 
254641     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_bounds2.proof 
254641     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 87.8ns 
254642     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
257407     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.76s 
257408     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_bounds2 
258278     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_bounds2 
258291     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 10ms 
258294     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_induction_upper2.proof 
258294     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 237.1ns 
258295     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
261049     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.75s 
261049     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_upper2 
261937     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_induction_upper2 
261940     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.05ms 
261942     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_induction_upper_concrete.proof 
261942     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 79.8ns 
261943     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
264698     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.76s 
264698     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_upper_concrete 
265612     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_induction_upper_concrete 
265616     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.93ms 
265617     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_induction_upper_concrete_2.proof 
265617     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 91.9ns 
265618     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
268355     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.74s 
268355     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_upper_concrete_2 
269271     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_induction_upper_concrete_2 
269276     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.19ms 
269278     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_induction_upper2_concrete.proof 
269278     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 77.2ns 
269278     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
272022     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.74s 
272022     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_upper2_concrete 
272923     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_induction_upper2_concrete 
272926     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 873.9ns 
272927     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_induction_lower_concrete.proof 
272927     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 66.3ns 
272928     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
275623     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.69s 
275623     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_lower_concrete 
276492     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_induction_lower_concrete 
276494     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 554.11ns 
276495     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_induction_lower2.proof 
276495     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 70.1ns 
276496     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
279237     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.74s 
279237     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_lower2 
280141     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_induction_lower2 
280144     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.81ms 
280146     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_induction_lower2_concrete.proof 
280146     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 102.1ns 
280147     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
282882     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.74s 
282882     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_lower2_concrete 
283803     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_induction_lower2_concrete 
283806     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 770.35ns 
283808     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_positive.proof 
283808     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 275.72ns 
283809     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
286610     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.8s 
286610     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_positive 
287497     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_positive 
287534     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 34.31ms 
287536     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_upper_bound.proof 
287536     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 198.01ns 
287537     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
290242     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.7s 
290242     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_upper_bound 
291145     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_upper_bound 
291182     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 33.56ms 
291185     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_lower_bound.proof 
291185     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 295.3ns 
291187     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
293946     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.76s 
293946     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_lower_bound 
294825     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_lower_bound 
294847     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 20.11ms 
294849     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_positive_lower_bound_element.proof 
294849     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 67ns 
294850     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
297603     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.75s 
297603     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_positive_lower_bound_element 
298519     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_positive_lower_bound_element 
298577     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 53.73ms 
298578     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_sub_same_index.proof 
298578     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 82.8ns 
298579     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
301322     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.74s 
301322     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_sub_same_index 
302220     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_sub_same_index 
302243     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 19.66ms 
302244     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_less_same_index.proof 
302245     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 80.91ns 
302245     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
304927     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.68s 
304928     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_less_same_index 
305828     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_less_same_index 
305864     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 32.28ms 
305866     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_equal_except_one_index.proof 
305866     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 75.5ns 
305867     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
308572     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.71s 
308572     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_equal_except_one_index 
309470     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_equal_except_one_index 
309490     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 16.09ms 
309491     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_is_max.proof 
309491     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 78.8ns 
309492     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
312249     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.76s 
312250     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_is_max 
313131     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_is_max 
313147     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 12.76ms 
313148     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_is_max2.proof 
313148     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 73.6ns 
313149     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
315907     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.76s 
315907     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_is_max2 
316827     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_is_max2 
316844     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 13.89ms 
316846     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_is_max3.proof 
316846     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 72.5ns 
316847     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
319540     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.69s 
319540     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_is_max3 
320422     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_is_max3 
320437     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 11.5ms 
320439     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_is_max4.proof 
320439     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 226.41ns 
320440     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
323143     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.7s 
323143     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_is_max4 
324069     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_is_max4 
324089     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 16.5ms 
324090     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_lt_max.proof 
324090     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 79.6ns 
324091     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
326861     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.77s 
326861     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_lt_max 
327766     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_lt_max 
327784     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 15.22ms 
327785     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_lt_max2.proof 
327786     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 82.8ns 
327786     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
330590     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.8s 
330591     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_lt_max2 
331532     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_lt_max2 
331551     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 15.74ms 
331553     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_lt_max3.proof 
331553     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 77.7ns 
331554     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
334259     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.7s 
334259     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_lt_max3 
335155     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_lt_max3 
335180     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 18.9ms 
335184     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_lt_max4.proof 
335185     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 666.62ns 
335186     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
337893     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.71s 
337894     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_lt_max4 
338814     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_lt_max4 
338830     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 13.36ms 
338832     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_gt0.proof 
338832     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 69.2ns 
338833     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
341547     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.71s 
341547     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_gt0 
342470     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_gt0 
342488     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 14.81ms 
342490     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_gt0_alt.proof 
342491     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 261.61ns 
342492     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
345145     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.65s 
345145     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_gt0_alt 
345958     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_gt0_alt 
345975     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 13.99ms 
345976     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_add_concrete.proof 
345976     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 61.1ns 
345977     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
348652     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.68s 
348652     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_add_concrete 
349510     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_add_concrete 
349516     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.03ms 
349521     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bprod/Taclet_bprod_all_positive.proof 
349521     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 230.4ns 
349522     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
352243     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.72s 
352243     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bprod_all_positive 
353111     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bprod_all_positive 
353124     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 9.96ms 
353125     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bprod/Taclet_bprod_split.proof 
353125     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 59.7ns 
353126     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
355746     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.62s 
355746     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bprod_split 
356619     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bprod_split 
356623     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.99ms 
356624     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powConcrete0.proof 
356624     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 75.2ns 
356625     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
359338     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.71s 
359339     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powConcrete0 
360308     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powConcrete0 
360311     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 629.02ns 
360312     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powConcrete1.proof 
360312     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 67.3ns 
360313     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
363299     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.99s 
363299     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powConcrete1 
364211     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powConcrete1 
364214     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 733.52ns 
364215     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powSplitFactor.proof 
364215     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 56ns 
364216     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
367030     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.81s 
367030     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powSplitFactor 
368008     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powSplitFactor 
368014     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.78ms 
368015     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powAdd.proof 
368016     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 57.5ns 
368016     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
370852     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.84s 
370852     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powAdd 
371766     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powAdd 
371772     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.03ms 
371773     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powMono.proof 
371774     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 72.2ns 
371774     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
374540     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.77s 
374540     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powMono 
375460     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powMono 
375473     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 10.65ms 
375475     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powMonoConcrete.proof 
375475     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 77ns 
375476     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
378348     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.87s 
378348     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powMonoConcrete 
379221     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powMonoConcrete 
379224     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.75ms 
379225     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powMonoConcreteRight.proof 
379225     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 53.6ns 
379226     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
381919     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.69s 
381919     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powMonoConcreteRight 
382792     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powMonoConcreteRight 
382794     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 512.62ns 
382795     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powPositive.proof 
382795     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 57.5ns 
382796     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
385501     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.71s 
385501     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powPositive 
386400     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powPositive 
386405     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.05ms 
386406     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powPositiveConcrete.proof 
386406     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 67.2ns 
386407     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
389148     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.74s 
389148     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powPositiveConcrete 
390077     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powPositiveConcrete 
390080     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 589.41ns 
390081     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powGeq1Concrete.proof 
390082     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 257.81ns 
390083     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
392961     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.88s 
392961     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powGeq1Concrete 
393884     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powGeq1Concrete 
393886     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 588.91ns 
393887     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_pow2InIntLower.proof 
393887     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 64.5ns 
393888     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
396681     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.79s 
396681     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: pow2InIntLower 
397574     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: pow2InIntLower 
397576     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 587.92ns 
397578     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_pow2InIntUpper.proof 
397578     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 67.6ns 
397579     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
400333     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.75s 
400334     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: pow2InIntUpper 
401243     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: pow2InIntUpper 
401247     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.84ms 
401248     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logSelfConcrete.proof 
401249     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 122ns 
401249     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
403977     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.73s 
403977     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logSelfConcrete 
404920     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logSelfConcrete 
404928     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 5.35ms 
404929     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_log1Concrete.proof 
404929     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 55.4ns 
404930     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
407640     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.71s 
407640     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: log1Concrete 
408556     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: log1Concrete 
408559     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.77ms 
408561     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logProduct.proof 
408561     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 65.5ns 
408562     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
411350     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.79s 
411350     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logProduct 
412272     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logProduct 
412278     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.88ms 
412280     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logTimesBaseConcrete.proof 
412280     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 57.3ns 
412281     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
415037     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.76s 
415037     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logTimesBaseConcrete 
415908     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logTimesBaseConcrete 
415913     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.23ms 
415914     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logProdIdentity.proof 
415914     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 70.6ns 
415915     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
418657     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.74s 
418657     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logProdIdentity 
419558     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logProdIdentity 
419573     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 11.69ms 
419575     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logProdIdentityConcrete.proof 
419575     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 91.2ns 
419576     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
422389     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.81s 
422389     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logProdIdentityConcrete 
423308     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logProdIdentityConcrete 
423312     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.85ms 
423313     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logPowIdentity.proof 
423313     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 60.7ns 
423314     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
426017     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.7s 
426017     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logPowIdentity 
426924     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logPowIdentity 
426927     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.07ms 
426928     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logPowIdentityConcrete.proof 
426928     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 58ns 
426929     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
429696     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.77s 
429696     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logPowIdentityConcrete 
430604     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logPowIdentityConcrete 
430608     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.01ms 
430609     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logPositive.proof 
430609     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 57.4ns 
430610     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
433418     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.81s 
433418     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logPositive 
434317     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logPositive 
434336     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 16.14ms 
434338     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logPositiveConcrete.proof 
434338     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 99.9ns 
434339     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
437161     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.82s 
437161     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logPositiveConcrete 
438077     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logPositiveConcrete 
438081     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 515.41ns 
438083     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logMono.proof 
438084     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 73.9ns 
438084     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
440855     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.77s 
440855     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logMono 
441786     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logMono 
441827     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 33.57ms 
441828     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logMonoConcrete.proof 
441828     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 76.4ns 
441829     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
444580     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.75s 
444580     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logMonoConcrete 
445478     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logMonoConcrete 
445482     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.47ms 
445483     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powLogLess.proof 
445483     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 55.9ns 
445484     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
448243     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.76s 
448243     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powLogLess 
449125     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powLogLess 
449142     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 13.73ms 
449143     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powLogMore2.proof 
449143     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 70.4ns 
449144     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
451915     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.77s 
451915     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powLogMore2 
452835     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powLogMore2 
452854     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 15.92ms 
452855     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logLessThanPow.proof 
452856     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 75.7ns 
452856     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
455566     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.71s 
455566     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logLessThanPow 
456462     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logLessThanPow 
456483     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 16.87ms 
456484     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logLessThanPowConcrete.proof 
456484     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 75.1ns 
456485     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
459195     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.71s 
459195     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logLessThanPowConcrete 
460105     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logLessThanPowConcrete 
460107     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 488.11ns 
460109     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logSqueeze.proof 
460109     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 56.8ns 
460110     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
462940     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.83s 
462941     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logSqueeze 
463924     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logSqueeze 
463930     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.59ms 
463931     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/booleanRules/Taclet_ifthenelse_equals.proof 
463931     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 59.1ns 
463932     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
466662     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.73s 
466662     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: ifthenelse_equals 
467593     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: ifthenelse_equals 
467597     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.56ms 
467599     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/booleanRules/Taclet_ifthenelse_equals_1.proof 
467599     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 180.3ns 
467600     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
470411     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.81s 
470411     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: ifthenelse_equals_1 
471332     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: ifthenelse_equals_1 
471335     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 782.91ns 
471336     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/booleanRules/Taclet_ifthenelse_equals_2.proof 
471336     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 55.9ns 
471337     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
474115     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.78s 
474115     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: ifthenelse_equals_2 
475016     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: ifthenelse_equals_2 
475019     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 721.21ns 
475020     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/locSet/Taclet_disjointWithSingleton1.proof 
475020     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 56.2ns 
475021     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
477831     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.81s 
477831     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: disjointWithSingleton1 
478763     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: disjointWithSingleton1 
478766     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.28ms 
478768     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/locSet/Taclet_disjointWithSingleton2.proof 
478768     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 131.8ns 
478769     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
481536     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.77s 
481536     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: disjointWithSingleton2 
482424     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: disjointWithSingleton2 
482427     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.24ms 
482429     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/locSet/Taclet_disjointArrayRanges.proof 
482429     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 171.2ns 
482430     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
485134     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.7s 
485135     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: disjointArrayRanges 
486008     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: disjointArrayRanges 
486017     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 5.95ms 
486018     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/locSet/Taclet_disjointArrayRangeAllFields1.proof 
486018     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 69.3ns 
486019     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
488735     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.72s 
488735     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: disjointArrayRangeAllFields1 
489658     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: disjointArrayRangeAllFields1 
489665     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 5.33ms 
489667     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/locSet/Taclet_disjointArrayRangeAllFields2.proof 
489667     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 58.6ns 
489667     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
492410     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.74s 
492410     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: disjointArrayRangeAllFields2 
493335     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: disjointArrayRangeAllFields2 
493342     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 5.18ms 
493344     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqSelfDefinition.proof 
493344     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 62.4ns 
493345     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
496233     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.89s 
496233     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqSelfDefinition 
497249     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqSelfDefinition 
497269     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 17.44ms 
497270     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqOutsideValue.proof 
497270     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 62ns 
497271     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
500089     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.82s 
500089     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqOutsideValue 
501076     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqOutsideValue 
501081     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.52ms 
501083     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_castedGetAny.proof 
501083     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 216.1ns 
501084     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
504016     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.93s 
504016     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: castedGetAny 
504898     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: castedGetAny 
504903     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.57ms 
504904     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqGetAlphaCast.proof 
504904     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 56.4ns 
504905     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
507654     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.75s 
507654     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqGetAlphaCast 
508592     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqGetAlphaCast 
508595     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 826.21ns 
508598     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqSingleton.proof 
508598     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 234.2ns 
508599     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
511376     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.78s 
511376     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqSingleton 
512335     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqSingleton 
512338     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.02ms 
512340     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqSingletonConcrete.proof 
512341     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 236.6ns 
512341     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
515127     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.79s 
515127     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqSingletonConcrete 
516038     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqSingletonConcrete 
516041     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 984.82ns 
516042     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqConcat.proof 
516042     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 75.6ns 
516043     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
518754     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.71s 
518755     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqConcat 
519714     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqConcat 
519724     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 7.05ms 
519725     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqSub.proof 
519725     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 72.9ns 
519726     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
522491     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.77s 
522492     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqSub 
523401     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqSub 
523404     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.25ms 
523405     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqReverse.proof 
523405     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 72.8ns 
523406     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
526084     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.68s 
526084     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqReverse 
526948     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqReverse 
526953     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.87ms 
526955     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqEmpty.proof 
526955     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 84ns 
526955     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
529599     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.64s 
529600     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqEmpty 
530515     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqEmpty 
530518     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 822.91ns 
530520     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqSingleton.proof 
530520     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 88.2ns 
530521     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
533264     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.74s 
533265     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqSingleton 
534200     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqSingleton 
534202     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 667.21ns 
534203     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqConcat.proof 
534203     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 61.5ns 
534204     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
536978     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.77s 
536978     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqConcat 
537867     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqConcat 
537870     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.48ms 
537872     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqSub.proof 
537872     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 76.8ns 
537873     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
540544     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.67s 
540545     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqSub 
541434     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqSub 
541436     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 889.91ns 
541438     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqReverse.proof 
541438     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 66.7ns 
541438     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
544275     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.84s 
544275     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqReverse 
545274     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqReverse 
545277     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.1ms 
545278     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_equalityToSeqGetAndSeqLenLeft.proof 
545278     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 57.4ns 
545279     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
548023     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.74s 
548023     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: equalityToSeqGetAndSeqLenLeft 
548955     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: equalityToSeqGetAndSeqLenLeft 
548957     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.05ms 
548958     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_equalityToSeqGetAndSeqLenRight.proof 
548959     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 66.6ns 
548959     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
551711     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.75s 
551711     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: equalityToSeqGetAndSeqLenRight 
552641     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: equalityToSeqGetAndSeqLenRight 
552645     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.21ms 
552646     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqSingletonEQ.proof 
552646     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 74.4ns 
552647     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
555431     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.78s 
555432     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqSingletonEQ 
556357     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqSingletonEQ 
556359     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 858.61ns 
556361     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqConcatEQ.proof 
556361     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 63ns 
556362     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
559233     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.87s 
559233     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqConcatEQ 
560209     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqConcatEQ 
560219     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 7.89ms 
560220     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqSubEQ.proof 
560220     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 68.8ns 
560221     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
562963     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.74s 
562963     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqSubEQ 
563856     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqSubEQ 
563858     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 546.41ns 
563859     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqReverseEQ.proof 
563859     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 68.7ns 
563860     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
566557     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.7s 
566557     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqReverseEQ 
567475     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqReverseEQ 
567480     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.74ms 
567482     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqEmptyEQ.proof 
567482     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 60.2ns 
567483     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
570292     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.81s 
570292     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqEmptyEQ 
571212     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqEmptyEQ 
571215     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 917.61ns 
571217     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqSingletonEQ.proof 
571217     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 66.7ns 
571218     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
573979     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.76s 
573979     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqSingletonEQ 
574901     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqSingletonEQ 
574904     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 825.01ns 
574905     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqConcatEQ.proof 
574905     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 72ns 
574906     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
577606     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.7s 
577606     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqConcatEQ 
578530     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqConcatEQ 
578535     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.08ms 
578537     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqSubEQ.proof 
578538     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 215.4ns 
578538     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
581295     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.76s 
581295     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqSubEQ 
582196     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqSubEQ 
582198     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.09ms 
582200     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqReverseEQ.proof 
582200     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 70.6ns 
582201     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
584938     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.74s 
584938     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqReverseEQ 
585854     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqReverseEQ 
585857     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.43ms 
585858     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqDefEQ.proof 
585858     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 66.2ns 
585859     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
588621     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.76s 
588621     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqDefEQ 
589535     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqDefEQ 
589538     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.08ms 
589539     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqDefEQ.proof 
589539     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 54.3ns 
589540     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
592312     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.77s 
592312     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqDefEQ 
593235     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqDefEQ 
593239     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.14ms 
593240     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqConcatWithSeqEmpty1.proof 
593241     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 63.1ns 
593241     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
595965     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.72s 
595965     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqConcatWithSeqEmpty1 
596881     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqConcatWithSeqEmpty1 
596889     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 5.78ms 
596890     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqConcatWithSeqEmpty2.proof 
596890     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 62.3ns 
596891     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
599753     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.86s 
599753     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqConcatWithSeqEmpty2 
600706     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqConcatWithSeqEmpty2 
600714     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 6.44ms 
600716     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqReverseOfSeqEmpty.proof 
600716     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 74.2ns 
600717     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
603514     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.8s 
603514     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqReverseOfSeqEmpty 
604433     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqReverseOfSeqEmpty 
604440     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.75ms 
604441     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_subSeqComplete.proof 
604441     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 57.2ns 
604442     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
607262     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.82s 
607262     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: subSeqComplete 
608211     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: subSeqComplete 
608218     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.84ms 
608220     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_subSeqTailR.proof 
608220     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 59ns 
608221     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
611019     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.8s 
611019     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: subSeqTailR 
611962     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: subSeqTailR 
611973     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 8.71ms 
611974     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_subSeqTailL.proof 
611974     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 69.8ns 
611975     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
614743     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.77s 
614743     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: subSeqTailL 
615660     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: subSeqTailL 
615672     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 8.68ms 
615673     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_subSeqTailEQR.proof 
615673     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 68.5ns 
615674     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
618406     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.73s 
618407     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: subSeqTailEQR 
619299     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: subSeqTailEQR 
619309     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 8.21ms 
619311     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_subSeqTailEQL.proof 
619311     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 72.4ns 
619312     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
622083     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.77s 
622083     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: subSeqTailEQL 
623028     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: subSeqTailEQL 
623036     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 5.71ms 
623037     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDef_split.proof 
623037     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 68ns 
623038     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
625856     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.82s 
625856     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_split 
626806     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDef_split 
626828     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 18.66ms 
626830     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDef_induction_upper.proof 
626830     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 84.9ns 
626830     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
629671     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.84s 
629671     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_induction_upper 
630630     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDef_induction_upper 
630656     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 21.67ms 
630658     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDef_induction_upper_concrete.proof 
630659     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 237.6ns 
630660     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
633523     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.86s 
633524     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_induction_upper_concrete 
634483     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDef_induction_upper_concrete 
634505     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 18.41ms 
634507     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDef_induction_lower.proof 
634507     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 64.4ns 
634508     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
637318     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.81s 
637319     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_induction_lower 
638238     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDef_induction_lower 
638259     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 17.49ms 
638261     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDef_induction_lower_concrete.proof 
638261     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 103.6ns 
638262     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
641110     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.85s 
641110     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_induction_lower_concrete 
642063     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDef_induction_lower_concrete 
642084     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 17.79ms 
642086     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDef_split_in_three.proof 
642086     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 76.2ns 
642087     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
644900     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.81s 
644901     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_split_in_three 
645857     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDef_split_in_three 
645910     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 45.82ms 
645912     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDef_empty.proof 
645912     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 78.7ns 
645913     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
648768     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.85s 
648768     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_empty 
649722     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDef_empty 
649730     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.23ms 
649732     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDef_one_summand.proof 
649732     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 222.2ns 
649733     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
652563     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.83s 
652564     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_one_summand 
653519     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDef_one_summand 
653525     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.39ms 
653526     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDef_lower_equals_upper.proof 
653526     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 61.2ns 
653527     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
656405     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.88s 
656405     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_lower_equals_upper 
657383     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDef_lower_equals_upper 
657387     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.02ms 
657388     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDefOfSeq.proof 
657388     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 65.9ns 
657389     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
660240     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.85s 
660240     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDefOfSeq 
661203     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDefOfSeq 
661218     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 10.96ms 
661219     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqSelfDefinitionEQ2.proof 
661219     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 77.5ns 
661220     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
664152     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.93s 
664152     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqSelfDefinitionEQ2 
665113     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqSelfDefinitionEQ2 
665122     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 7.18ms 
665125     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_indexOfSeqSingleton.proof 
665125     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 251.7ns 
665126     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
668006     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.88s 
668006     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: indexOfSeqSingleton 
669046     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: indexOfSeqSingleton 
669049     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.42ms 
669050     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_indexOfSeqConcatFirst.proof 
669050     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 67.1ns 
669051     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
671897     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.85s 
671897     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: indexOfSeqConcatFirst 
672855     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: indexOfSeqConcatFirst 
672866     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 8.4ms 
672867     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_indexOfSeqConcatSecond.proof 
672867     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 72.6ns 
672868     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
675689     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.82s 
675689     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: indexOfSeqConcatSecond 
676616     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: indexOfSeqConcatSecond 
676659     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 40.9ms 
676661     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_indexOfSeqSub.proof 
676661     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 64.2ns 
676661     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
679498     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.84s 
679499     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: indexOfSeqSub 
680428     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: indexOfSeqSub 
680443     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 11.78ms 
680444     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfArray2seq.proof 
680444     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 74.7ns 
680445     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
683305     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.86s 
683305     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfArray2seq 
684238     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfArray2seq 
684242     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.01ms 
684244     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getAnyOfArray2seq.proof 
684244     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 74ns 
684244     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
687191     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.95s 
687191     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getAnyOfArray2seq 
688128     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getAnyOfArray2seq 
688133     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.24ms 
688135     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfArray2seq.proof 
688135     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 60ns 
688136     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
691001     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.87s 
691001     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfArray2seq 
691933     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfArray2seq 
691939     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.22ms 
691941     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_getAnyOfNPermInv.proof 
691941     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 79.8ns 
691942     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
694816     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.87s 
694818     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getAnyOfNPermInv 
695751     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getAnyOfNPermInv 
695759     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 5.17ms 
695760     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqNPermRange.proof 
695760     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 68.7ns 
695761     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
698623     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.86s 
698623     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqNPermRange 
699582     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqNPermRange 
699630     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 40.8ms 
699632     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermTrans.proof 
699632     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 79.6ns 
699632     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
702474     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.84s 
702474     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermTrans 
703430     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermTrans 
703451     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 16.99ms 
703452     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermRefl.proof 
703452     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 76ns 
703453     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
706285     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.83s 
706286     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermRefl 
707224     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermRefl 
707237     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 9.88ms 
707238     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermSplit.proof 
707238     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 77.9ns 
707239     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
710043     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.8s 
710044     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermSplit 
710988     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermSplit 
710990     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 177.3ns 
710992     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqNPermRight.proof 
710992     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 58.4ns 
710993     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
713809     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.82s 
713809     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqNPermRight 
714750     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqNPermRight 
714842     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 78.98ms 
714844     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermFromSwap.proof 
714844     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 64.4ns 
714845     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
717567     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.72s 
717567     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermFromSwap 
718490     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermFromSwap 
718525     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 30.45ms 
718527     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermTransAlt0.proof 
718527     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 64.4ns 
718528     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
721392     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.86s 
721392     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermTransAlt0 
722317     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermTransAlt0 
722319     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 240.3ns 
722321     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermTransAlt1.proof 
722321     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 54.6ns 
722321     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
725049     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.73s 
725049     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermTransAlt1 
725976     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermTransAlt1 
725978     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 198.8ns 
725979     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermTransAlt2.proof 
725979     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 69.8ns 
725980     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
728777     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.8s 
728777     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermTransAlt2 
729735     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermTransAlt2 
729736     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 219.8ns 
729738     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermTransAlt3.proof 
729738     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 54.5ns 
729738     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
732564     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.83s 
732564     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermTransAlt3 
733482     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermTransAlt3 
733484     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 390.71ns 
733485     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermForall.proof 
733485     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 57ns 
733486     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
736211     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.73s 
736211     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermForall 
737142     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermForall 
737237     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 92.81ms 
737239     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermExists.proof 
737239     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 96.6ns 
737240     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
739993     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.75s 
739994     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermExists 
740926     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermExists 
740977     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 48.92ms 
740979     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm2/Taclet_schiffl_lemma_2.proof 
740979     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 69.2ns 
740980     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
743876     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.9s 
743876     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: schiffl_lemma_2 
744908     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: schiffl_lemma_2 
744910     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.8ns 
744947     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 1: 'macro split-prop' on goal 0 (script from line 49) 
744984     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 2: 'rule allRight' on goal 3 (script from line 50) 
745000     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 3: 'rule allRight' on goal 4 (script from line 51) 
745006     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 4: 'macro split-prop' on goal 5 (script from line 52) 
745017     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 5: 'rule 'seqPermDefLeft'' on goal 11 (script from line 53) 
745018     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 6: 'rule 'andLeft'' on goal 12 (script from line 54) 
745020     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 7: 'rule 'exLeft'' on goal 13 (script from line 55) 
745021     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 8: 'macro split-prop' on goal 14 (script from line 56) 
745028     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 9: 'rule  seqNPermRange' on goal 16 (script from line 58) 
745029     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) 
745032     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 11: 'rule impLeft' on goal 18 (script from line 60) 
745034     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 12: 'tryclose branch' on goal 19 (script from line 61) 
745285     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 13: 'rule andLeft' on goal 20 (script from line 62) 
745286     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 14: 'rule andLeft' on goal 97 (script from line 63) 
745287     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) 
745288     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 16: 'rule impLeft' on goal 99 (script from line 66) 
745289     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 17: 'tryclose branch' on goal 100 (script from line 67) 
745452     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 18: 'rule andLeft' on goal 101 (script from line 68) 
745453     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 19: 'rule andLeft' on goal 188 (script from line 69) 
745457     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 20: 'rule seqNPermDefLeft' on goal 189 (script from line 71) 
745458     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) 
745459     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 22: 'rule impLeft' on goal 191 (script from line 73) 
745462     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 23: 'tryclose branch' on goal 192 (script from line 74) 
745670     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 24: 'rule exLeft' on goal 193 (script from line 75) 
745673     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 25: 'rule andLeft' on goal 310 (script from line 76) 
745674     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 26: 'rule andLeft' on goal 311 (script from line 77) 
745681     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) 
745682     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 28: 'rule impLeft' on goal 313 (script from line 80) 
745683     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 29: 'tryclose branch' on goal 314 (script from line 81) 
745855     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 30: 'rule exLeft' on goal 315 (script from line 82) 
745858     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 31: 'rule andLeft' on goal 420 (script from line 83) 
745859     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 32: 'rule andLeft' on goal 421 (script from line 84) 
745860     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) 
745860     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 34: 'rule impLeft' on goal 423 (script from line 87) 
745861     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 35: 'tryclose branch' on goal 424 (script from line 88) 
745872     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 36: 'rule andLeft' on goal 425 (script from line 89) 
745874     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 37: 'rule andLeft' on goal 434 (script from line 90) 
745876     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) 
745877     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) 
745878     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 40: 'rule impLeft' on goal 437 (script from line 94) 
745879     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 41: 'tryclose branch' on goal 438 (script from line 95) 
745890     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 42: 'rule andLeft' on goal 439 (script from line 96) 
745891     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 43: 'rule andLeft' on goal 448 (script from line 97) 
745893     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) 
745894     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) 
745894     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 46: 'rule impLeft' on goal 451 (script from line 101) 
745896     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 47: 'tryclose branch' on goal 452 (script from line 102) 
746083     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) 
746084     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 49: 'rule impLeft' on goal 562 (script from line 105) 
746086     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 50: 'tryclose branch' on goal 563 (script from line 106) 
746258     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) 
746259     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) 
746261     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 53: 'rule andRight' on goal 676 (script from line 112) 
746263     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 54: 'rule andRight' on goal 677 (script from line 113) 
746264     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 55: 'rule andRight' on goal 679 (script from line 114) 
746265     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 56: 'rule andRight' on goal 681 (script from line 115) 
746268     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 57: 'rule lenOfSwap' on goal 683 (script from line 116) 
746269     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 58: 'tryclose branch' on goal 685 (script from line 117) 
746274     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 59: 'rule seqNPermSwapNPerm' on goal 684 (script from line 119) 
746275     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) 
746276     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) 
746277     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 62: 'rule impLeft' on goal 689 (script from line 122) 
746278     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 63: 'tryclose branch' on goal 690 (script from line 123) 
746450     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 64: 'tryclose branch' on goal 691 (script from line 124) 
746454     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 65: 'rule allRight' on goal 682 (script from line 126) 
746455     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 66: 'rule impRight' on goal 796 (script from line 127) 
746456     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 67: 'rule andLeft' on goal 797 (script from line 128) 
746457     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) 
746457     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 69: 'rule impLeft' on goal 799 (script from line 130) 
746458     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 70: 'tryclose branch' on goal 800 (script from line 131) 
746595     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 71: 'rule getOfSwap' on goal 801 (script from line 132) 
746596     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 72: 'rule ifthenelse_negated' on goal 912 (script from line 133) 
746597     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 73: 'rule ifthenelse_split occ=0' on goal 913 (script from line 134) 
746598     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 74: 'rule andLeft' on goal 914 (script from line 135) 
746599     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 75: 'rule andLeft' on goal 916 (script from line 136) 
746600     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 76: 'rule andLeft' on goal 917 (script from line 137) 
746601     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 77: 'rule ifthenelse_split occ=0' on goal 918 (script from line 138) 
746602     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 78: 'tryclose branch' on goal 919 (script from line 139) 
746713     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 79: 'rule ifthenelse_split occ=0' on goal 920 (script from line 140) 
746714     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 80: 'tryclose branch' on goal 1011 (script from line 141) 
746850     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 81: 'tryclose branch' on goal 1012 (script from line 142) 
746857     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 82: 'tryclose branch' on goal 915 (script from line 143) 
746864     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 83: 'rule getOfSwap' on goal 680 (script from line 145) 
746865     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 84: 'rule ifthenelse_negated' on goal 1099 (script from line 146) 
746866     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 85: 'rule ifthenelse_split occ=0' on goal 1100 (script from line 147) 
746867     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 86: 'rule andLeft' on goal 1101 (script from line 148) 
746867     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 87: 'rule andLeft' on goal 1103 (script from line 149) 
746868     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 88: 'rule andLeft' on goal 1104 (script from line 150) 
746868     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 89: 'rule ifthenelse_split occ=0' on goal 1105 (script from line 151) 
746868     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 90: 'tryclose branch' on goal 1106 (script from line 152) 
746880     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 91: 'tryclose branch' on goal 1107 (script from line 153) 
746888     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 92: 'tryclose branch' on goal 1102 (script from line 154) 
747006     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 93: 'rule getOfSwap' on goal 678 (script from line 156) 
747007     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 94: 'rule ifthenelse_negated' on goal 1225 (script from line 157) 
747007     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 95: 'rule ifthenelse_split occ=0' on goal 1226 (script from line 158) 
747008     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 96: 'rule andLeft' on goal 1227 (script from line 159) 
747009     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 97: 'rule andLeft' on goal 1229 (script from line 160) 
747009     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 98: 'rule andLeft' on goal 1230 (script from line 161) 
747010     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 99: 'rule ifthenelse_split occ=0' on goal 1231 (script from line 162) 
747010     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 100: 'tryclose branch' on goal 1232 (script from line 163) 
747069     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 101: 'tryclose branch' on goal 1233 (script from line 164) 
747076     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 102: 'tryclose branch' on goal 1228 (script from line 165) 
747184     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) 
747184     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 104: 'rule seqNPermInjective' on goal 1397 (script from line 169) 
747185     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) 
747187     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) 
747188     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 107: 'rule impLeft' on goal 1401 (script from line 172) 
747189     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 108: 'tryclose branch' on goal 1402 (script from line 173) 
747334     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 109: 'tryclose branch' on goal 1403 (script from line 174) 
747339     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) 
747340     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) 
747340     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 112: 'rule andRight' on goal 1536 (script from line 180) 
747342     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 113: 'rule andRight' on goal 1537 (script from line 181) 
747343     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 114: 'rule andRight' on goal 1539 (script from line 182) 
747343     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 115: 'rule andRight' on goal 1541 (script from line 183) 
747344     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 116: 'tryclose branch' on goal 1543 (script from line 184) 
747355     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 117: 'rule seqNPermSwapNPerm' on goal 1544 (script from line 186) 
747356     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) 
747357     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) 
747358     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 120: 'tryclose branch' on goal 1560 (script from line 189) 
747471     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 121: 'rule allRight' on goal 1542 (script from line 191) 
747472     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 122: 'rule impRight' on goal 1667 (script from line 192) 
747473     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 123: 'rule andLeft' on goal 1668 (script from line 193) 
747474     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) 
747475     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 125: 'rule impLeft' on goal 1670 (script from line 195) 
747476     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 126: 'tryclose branch' on goal 1671 (script from line 196) 
747595     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 127: 'rule getOfSwap' on goal 1672 (script from line 197) 
747597     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 128: 'rule ifthenelse_negated' on goal 1786 (script from line 198) 
747598     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 129: 'rule ifthenelse_split occ=0' on goal 1787 (script from line 199) 
747599     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 130: 'rule andLeft' on goal 1788 (script from line 200) 
747600     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 131: 'rule andLeft' on goal 1790 (script from line 201) 
747600     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 132: 'rule andLeft' on goal 1791 (script from line 202) 
747601     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 133: 'rule ifthenelse_split occ=0' on goal 1792 (script from line 203) 
747602     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 134: 'tryclose branch' on goal 1793 (script from line 204) 
747695     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 135: 'rule ifthenelse_split occ=0' on goal 1794 (script from line 205) 
747697     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 136: 'tryclose branch' on goal 1885 (script from line 206) 
747778     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) 
747779     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 138: 'rule impLeft' on goal 1968 (script from line 208) 
747780     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 139: 'tryclose branch' on goal 1969 (script from line 209) 
747785     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 140: 'tryclose branch' on goal 1970 (script from line 210) 
747790     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 141: 'tryclose branch' on goal 1789 (script from line 211) 
747794     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 142: 'tryclose branch' on goal 1540 (script from line 212) 
747923     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 143: 'rule getOfSwap' on goal 1538 (script from line 214) 
747924     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 144: 'rule ifthenelse_negated' on goal 2097 (script from line 215) 
747925     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 145: 'rule ifthenelse_split occ=0' on goal 2098 (script from line 216) 
747927     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 146: 'tryclose branch' on goal 2099 (script from line 217) 
747939     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 147: 'tryclose branch' on goal 2100 (script from line 218) 
748036     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 148: 'tryclose branch' on goal 1535 (script from line 220) 
751984     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) 
751985     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) 
751989     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 151: 'rule andRight' on goal 4268 (script from line 227) 
751991     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 152: 'rule andRight' on goal 4269 (script from line 228) 
751992     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 153: 'rule andRight' on goal 4271 (script from line 229) 
751993     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 154: 'rule andRight' on goal 4273 (script from line 230) 
751993     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 155: 'tryclose branch' on goal 4275 (script from line 231) 
752002     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 156: 'rule seqNPermSwapNPerm' on goal 4276 (script from line 233) 
752003     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) 
752004     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) 
752007     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 159: 'rule impLeft' on goal 4289 (script from line 236) 
752007     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 160: 'tryclose branch' on goal 4290 (script from line 237) 
752113     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 161: 'tryclose branch' on goal 4291 (script from line 238) 
752118     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 162: 'rule allRight' on goal 4274 (script from line 240) 
752119     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 163: 'rule impRight' on goal 4400 (script from line 241) 
752120     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 164: 'rule andLeft' on goal 4401 (script from line 242) 
752120     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) 
752121     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 166: 'rule impLeft' on goal 4403 (script from line 244) 
752122     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 167: 'tryclose branch' on goal 4404 (script from line 245) 
752229     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 168: 'rule getOfSwap' on goal 4405 (script from line 246) 
752230     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 169: 'rule ifthenelse_negated' on goal 4521 (script from line 247) 
752232     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 170: 'rule ifthenelse_split occ=0' on goal 4522 (script from line 248) 
752233     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 171: 'rule andLeft' on goal 4523 (script from line 249) 
752234     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 172: 'rule andLeft' on goal 4525 (script from line 250) 
752234     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 173: 'rule andLeft' on goal 4526 (script from line 251) 
752235     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 174: 'rule ifthenelse_split occ=0' on goal 4527 (script from line 252) 
752236     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 175: 'tryclose branch' on goal 4528 (script from line 253) 
752320     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 176: 'rule ifthenelse_split occ=0' on goal 4529 (script from line 254) 
752321     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 177: 'tryclose branch' on goal 4622 (script from line 255) 
752402     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 178: 'tryclose branch' on goal 4623 (script from line 256) 
752408     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 179: 'tryclose branch' on goal 4524 (script from line 257) 
752413     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 180: 'rule getOfSwap' on goal 4272 (script from line 259) 
752414     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 181: 'rule ifthenelse_negated' on goal 4713 (script from line 260) 
752415     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 182: 'rule ifthenelse_split occ=0' on goal 4714 (script from line 261) 
752416     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 183: 'tryclose branch' on goal 4715 (script from line 262) 
752427     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 184: 'tryclose branch' on goal 4716 (script from line 263) 
752519     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 185: 'rule getOfSwap' on goal 4270 (script from line 265) 
752520     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 186: 'rule ifthenelse_negated' on goal 4839 (script from line 266) 
752521     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 187: 'rule ifthenelse_split occ=0' on goal 4840 (script from line 267) 
752522     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 188: 'tryclose branch' on goal 4841 (script from line 268) 
752603     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 189: 'tryclose branch' on goal 4842 (script from line 269) 
752614     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) 
752615     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) 
752616     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 192: 'rule andRight' on goal 4950 (script from line 276) 
752617     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 193: 'rule andRight' on goal 4951 (script from line 277) 
752618     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 194: 'rule andRight' on goal 4953 (script from line 278) 
752618     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 195: 'rule andRight' on goal 4955 (script from line 279) 
752619     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 196: 'tryclose branch' on goal 4957 (script from line 280) 
752631     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 197: 'rule seqNPermSwapNPerm' on goal 4958 (script from line 282) 
752632     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) 
752633     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) 
752634     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 200: 'rule impLeft' on goal 4979 (script from line 285) 
752635     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 201: 'tryclose branch' on goal 4980 (script from line 286) 
752734     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) 
752735     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) 
752736     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) 
752737     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 205: 'rule impLeft' on goal 5095 (script from line 290) 
752738     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 206: 'tryclose branch' on goal 5096 (script from line 291) 
752842     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 207: 'tryclose branch' on goal 5097 (script from line 292) 
752847     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 208: 'rule allRight' on goal 4956 (script from line 294) 
752848     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 209: 'rule impRight' on goal 5212 (script from line 295) 
752849     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 210: 'rule andLeft' on goal 5213 (script from line 296) 
752850     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) 
752851     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 212: 'rule impLeft' on goal 5215 (script from line 300) 
752852     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 213: 'tryclose branch' on goal 5216 (script from line 301) 
752963     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 214: 'rule getOfSwap' on goal 5217 (script from line 303) 
752964     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 215: 'rule ifthenelse_negated' on goal 5337 (script from line 304) 
752965     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 216: 'rule ifthenelse_split occ=0' on goal 5338 (script from line 305) 
752966     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 217: 'rule andLeft' on goal 5339 (script from line 306) 
752967     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 218: 'rule andLeft' on goal 5341 (script from line 307) 
752968     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 219: 'rule andLeft' on goal 5342 (script from line 308) 
752969     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 220: 'rule ifthenelse_split occ=0' on goal 5343 (script from line 309) 
752969     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 221: 'rule getOfSwap' on goal 5344 (script from line 310) 
752970     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 222: 'rule ifthenelse_negated' on goal 5346 (script from line 311) 
752971     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 223: 'rule ifthenelse_split occ=0' on goal 5347 (script from line 312) 
752972     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 224: 'rule andLeft' on goal 5348 (script from line 313) 
752973     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 225: 'rule andLeft' on goal 5350 (script from line 314) 
752974     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 226: 'rule andLeft' on goal 5351 (script from line 315) 
752974     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 227: 'rule ifthenelse_split occ=0' on goal 5352 (script from line 316) 
752975     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 228: 'tryclose branch' on goal 5353 (script from line 317) 
753073     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 229: 'rule ifthenelse_split occ=0' on goal 5354 (script from line 318) 
753075     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 230: 'tryclose branch' on goal 5463 (script from line 319) 
753082     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 231: 'tryclose branch' on goal 5464 (script from line 320) 
753167     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 232: 'tryclose branch' on goal 5349 (script from line 321) 
753308     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 233: 'rule ifthenelse_split' on goal 5345 (script from line 323) 
753310     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 234: 'rule getOfSwap' on goal 5660 (script from line 324) 
753311     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 235: 'rule ifthenelse_negated' on goal 5662 (script from line 325) 
753312     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 236: 'rule ifthenelse_split occ=0' on goal 5663 (script from line 326) 
753313     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 237: 'rule andLeft' on goal 5664 (script from line 327) 
753314     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 238: 'rule andLeft' on goal 5666 (script from line 328) 
753314     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 239: 'rule andLeft' on goal 5667 (script from line 329) 
753315     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 240: 'rule ifthenelse_split occ=0' on goal 5668 (script from line 330) 
753315     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 241: 'tryclose branch' on goal 5669 (script from line 331) 
753411     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 242: 'tryclose branch' on goal 5670 (script from line 332) 
753418     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 243: 'tryclose branch' on goal 5665 (script from line 333) 
753521     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 244: 'rule getOfSwap' on goal 5661 (script from line 335) 
753522     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 245: 'rule ifthenelse_negated' on goal 5887 (script from line 336) 
753523     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 246: 'rule ifthenelse_split occ=0' on goal 5888 (script from line 337) 
753524     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 247: 'rule andLeft' on goal 5889 (script from line 338) 
753525     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 248: 'rule andLeft' on goal 5891 (script from line 339) 
753525     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 249: 'rule andLeft' on goal 5892 (script from line 340) 
753526     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 250: 'rule ifthenelse_split occ=0' on goal 5893 (script from line 341) 
753526     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 251: 'tryclose branch' on goal 5894 (script from line 342) 
753532     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 252: 'rule ifthenelse_split occ=0' on goal 5895 (script from line 343) 
753533     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 253: 'tryclose branch' on goal 5897 (script from line 344) 
753623     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 254: 'tryclose branch' on goal 5898 (script from line 345) 
753629     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 255: 'tryclose branch' on goal 5890 (script from line 346) 
753635     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 256: 'tryclose branch' on goal 5340 (script from line 347) 
753749     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 257: 'rule getOfSwap' on goal 4954 (script from line 349) 
753750     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 258: 'rule ifthenelse_negated' on goal 6115 (script from line 350) 
753751     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 259: 'rule ifthenelse_split occ=0' on goal 6116 (script from line 351) 
753752     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 260: 'rule andLeft' on goal 6117 (script from line 352) 
753752     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 261: 'rule andLeft' on goal 6119 (script from line 353) 
753753     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 262: 'rule andLeft' on goal 6120 (script from line 354) 
753753     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 263: 'rule ifthenelse_split occ=0' on goal 6121 (script from line 355) 
753754     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 264: 'tryclose branch' on goal 6122 (script from line 356) 
753816     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 265: 'rule ifthenelse_split occ=0' on goal 6123 (script from line 357) 
753817     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 266: 'rule getOfSwap' on goal 6193 (script from line 358) 
753818     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 267: 'rule ifthenelse_negated' on goal 6195 (script from line 359) 
753819     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 268: 'rule ifthenelse_split occ=0' on goal 6196 (script from line 360) 
753819     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 269: 'tryclose branch' on goal 6197 (script from line 361) 
753826     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 270: 'tryclose branch' on goal 6198 (script from line 362) 
753832     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 271: 'tryclose branch' on goal 6194 (script from line 363) 
753963     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 272: 'tryclose branch' on goal 6118 (script from line 364) 
754059     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 273: 'rule getOfSwap' on goal 4952 (script from line 366) 
754060     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 274: 'rule ifthenelse_negated' on goal 6456 (script from line 367) 
754061     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 275: 'rule ifthenelse_split occ=0' on goal 6457 (script from line 368) 
754062     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 276: 'tryclose branch' on goal 6458 (script from line 369) 
754250     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 277: 'tryclose branch' on goal 6459 (script from line 370) 
754349     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) 
754350     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 279: 'tryclose branch' on goal 6735 (script from line 377) 
757730     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 280: 'rule seqNPermSwapNPerm' on goal 6735 (script from line 379) 
757735     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) 
757736     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) 
757736     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 283: 'rule impLeft' on goal 8785 (script from line 382) 
757737     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 284: 'tryclose branch' on goal 8786 (script from line 383) 
757863     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) 
757864     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) 
757865     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) 
757865     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 288: 'rule impLeft' on goal 8911 (script from line 387) 
757866     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 289: 'tryclose branch' on goal 8912 (script from line 388) 
757985     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 290: 'tryclose branch' on goal 8913 (script from line 389) 
761348     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 291: 'tryclose branch' on goal 6736 (script from line 396) 
764967     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 292: 'rule seqNPermSwapNPerm formula='seqNPerm(s_0)'' on goal 6736 (script from line 398) 
764971     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) 
764972     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) 
764973     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 295: 'rule impLeft' on goal 12635 (script from line 401) 
764973     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 296: 'tryclose branch' on goal 12636 (script from line 402) 
765102     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) 
765103     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) 
765104     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) 
765105     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) 
765106     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 301: 'tryclose branch' on goal 12760 (script from line 407) 
766383     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm2/Taclet_schiffl_thm_1.proof 
766383     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 98.5ns 
766384     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
769255     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.87s 
769255     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: schiffl_thm_1 
770200     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: schiffl_thm_1 
770201     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 6.9ns 
770202     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 1: 'macro split-prop' on goal 0 (script from line 50) 
770208     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) 
770218     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) 
770221     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) 
770223     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 5: 'rule impLeft' on goal 13 (script from line 54) 
770225     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 6: 'tryclose branch' on goal 14 (script from line 55) 
770229     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 7: 'rule exLeft' on goal 15 (script from line 56) 
770229     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 8: 'macro split-prop' on goal 23 (script from line 57) 
770233     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 9: 'rule seqPermDef occ=1' on goal 27 (script from line 58) 
770234     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 10: 'rule andRight' on goal 28 (script from line 59) 
770236     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 11: 'tryclose branch' on goal 29 (script from line 60) 
770245     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) 
770246     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 13: 'rule andRight' on goal 46 (script from line 62) 
770247     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 14: 'tryclose branch' on goal 47 (script from line 63) 
770298     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 15: 'rule allRight' on goal 48 (script from line 64) 
770298     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 16: 'rule impRight' on goal 119 (script from line 65) 
770299     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) 
770299     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 18: 'rule impLeft' on goal 121 (script from line 67) 
770300     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 19: 'tryclose branch' on goal 122 (script from line 68) 
770374     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 20: 'rule andLeft' on goal 123 (script from line 69) 
770374     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 21: 'rule seqNPermRange' on goal 203 (script from line 70) 
770376     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) 
770377     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 23: 'rule impLeft' on goal 205 (script from line 72) 
770378     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 24: 'tryclose branch' on goal 206 (script from line 73) 
770382     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 25: 'rule andLeft' on goal 207 (script from line 74) 
770383     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 26: 'rule andLeft' on goal 215 (script from line 75) 
770383     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 27: 'rule seqNPermRange' on goal 216 (script from line 76) 
770384     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) 
770385     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 29: 'rule impLeft' on goal 218 (script from line 78) 
770386     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 30: 'tryclose branch' on goal 219 (script from line 79) 
770480     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 31: 'rule andLeft' on goal 220 (script from line 80) 
770481     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 32: 'rule andLeft' on goal 311 (script from line 81) 
770482     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 33: 'rule seqNPermRange' on goal 312 (script from line 82) 
770482     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) 
770484     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 35: 'rule impLeft' on goal 314 (script from line 84) 
770485     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 36: 'tryclose branch' on goal 315 (script from line 85) 
770582     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 37: 'rule andLeft' on goal 316 (script from line 86) 
770583     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 38: 'rule andLeft' on goal 410 (script from line 87) 
770584     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 39: 'rule getOfSeqDef occ=0' on goal 411 (script from line 88) 
770585     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 40: 'rule getOfSeqDef' on goal 412 (script from line 89) 
770585     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 41: 'rule ifthenelse_split occ=0' on goal 413 (script from line 90) 
770586     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 42: 'rule andLeft occ=0' on goal 414 (script from line 91) 
770587     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 43: 'rule sub_zero_2 occ=0' on goal 416 (script from line 92) 
770587     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 44: 'rule ifthenelse_split occ=2' on goal 417 (script from line 93) 
770588     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 45: 'rule andLeft' on goal 418 (script from line 94) 
770589     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 46: 'rule sub_zero_2 occ=0' on goal 420 (script from line 95) 
770589     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 47: 'rule add_zero_right occ=0' on goal 421 (script from line 96) 
770590     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 48: 'rule add_zero_right occ=0' on goal 422 (script from line 97) 
770591     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 49: 'rule add_zero_right occ=0' on goal 423 (script from line 98) 
770591     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 50: 'rule add_zero_right occ=0' on goal 424 (script from line 99) 
770592     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 51: 'rule add_zero_right occ=0' on goal 425 (script from line 100) 
770592     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 52: 'rule add_zero_right occ=0' on goal 426 (script from line 101) 
770593     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 53: 'rule ifthenelse_split occ=0' on goal 427 (script from line 102) 
770594     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 54: 'rule ifthenelse_split occ=0' on goal 428 (script from line 103) 
770594     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 55: 'tryclose branch' on goal 430 (script from line 104) 
770597     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 56: 'tryclose branch' on goal 431 (script from line 105) 
770640     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 57: 'rule ifthenelse_split occ=0' on goal 429 (script from line 106) 
770641     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 58: 'tryclose branch' on goal 473 (script from line 107) 
770706     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 59: 'rule ifthenelse_split occ=0' on goal 474 (script from line 108) 
770707     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 60: 'rule seqNPermInjective' on goal 541 (script from line 109) 
770708     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) 
770709     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) 
770710     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 63: 'rule impLeft' on goal 545 (script from line 112) 
770711     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 64: 'tryclose branch' on goal 546 (script from line 113) 
770765     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 65: 'tryclose branch' on goal 547 (script from line 114) 
770768     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 66: 'rule ifthenelse_split occ=0' on goal 542 (script from line 115) 
770769     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 67: 'rule seqNPermInjective' on goal 606 (script from line 116) 
770769     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) 
770771     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) 
770772     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 70: 'rule impLeft' on goal 610 (script from line 119) 
770773     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 71: 'tryclose branch' on goal 611 (script from line 120) 
770825     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 72: 'tryclose branch' on goal 612 (script from line 121) 
770828     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 73: 'tryclose branch' on goal 607 (script from line 122) 
770832     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 74: 'tryclose branch' on goal 419 (script from line 123) 
770888     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 75: 'tryclose branch' on goal 415 (script from line 124) 
770949     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_eqSameSeq.proof 
770949     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 348.8ns 
770950     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
773938     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.99s 
773938     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: eqSameSeq 
774991     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: eqSameSeq 
775010     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 14.58ms