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

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

tests
0

failures
0

ignored
11m30.54s

duration
100%

successful

Tests

Test Method name Duration Result
powPositive data()[100] 3.358s passed
powPositiveConcrete data()[101] 3.349s passed
powGeq1Concrete data()[102] 3.344s passed
pow2InIntLower data()[103] 3.346s passed
pow2InIntUpper data()[104] 3.366s passed
logSelfConcrete data()[105] 3.354s passed
log1Concrete data()[106] 3.342s passed
logProduct data()[107] 3.339s passed
logTimesBaseConcrete data()[108] 3.346s passed
logProdIdentity data()[109] 3.372s passed
moduloByteIsInByte data()[10] 3.411s passed
logProdIdentityConcrete data()[110] 3.347s passed
logPowIdentity data()[111] 3.342s passed
logPowIdentityConcrete data()[112] 3.350s passed
logPositive data()[113] 3.375s passed
logPositiveConcrete data()[114] 3.338s passed
logMono data()[115] 3.357s passed
logMonoConcrete data()[116] 3.347s passed
powLogLess data()[117] 3.373s passed
powLogMore2 data()[118] 3.372s passed
logLessThanPow data()[119] 3.356s passed
moduloCharIsInChar data()[11] 3.408s passed
logLessThanPowConcrete data()[120] 3.340s passed
logSqueeze data()[121] 3.367s passed
ifthenelse_equals data()[122] 3.349s passed
ifthenelse_equals_1 data()[123] 3.347s passed
ifthenelse_equals_2 data()[124] 3.372s passed
disjointWithSingleton1 data()[125] 3.377s passed
disjointWithSingleton2 data()[126] 3.350s passed
disjointArrayRanges data()[127] 3.379s passed
disjointArrayRangeAllFields1 data()[128] 3.356s passed
disjointArrayRangeAllFields2 data()[129] 3.375s passed
div_unique1 data()[12] 3.469s passed
seqSelfDefinition data()[130] 3.359s passed
seqOutsideValue data()[131] 3.356s passed
castedGetAny data()[132] 3.369s passed
seqGetAlphaCast data()[133] 3.350s passed
getOfSeqSingleton data()[134] 3.369s passed
getOfSeqSingletonConcrete data()[135] 3.356s passed
getOfSeqConcat data()[136] 3.394s passed
getOfSeqSub data()[137] 3.359s passed
getOfSeqReverse data()[138] 3.358s passed
lenOfSeqEmpty data()[139] 3.381s passed
div_unique2 data()[13] 3.477s passed
lenOfSeqSingleton data()[140] 3.351s passed
lenOfSeqConcat data()[141] 3.381s passed
lenOfSeqSub data()[142] 3.351s passed
lenOfSeqReverse data()[143] 3.369s passed
equalityToSeqGetAndSeqLenLeft data()[144] 3.367s passed
equalityToSeqGetAndSeqLenRight data()[145] 3.353s passed
getOfSeqSingletonEQ data()[146] 3.387s passed
getOfSeqConcatEQ data()[147] 3.354s passed
getOfSeqSubEQ data()[148] 3.367s passed
getOfSeqReverseEQ data()[149] 3.353s passed
div_exists data()[14] 3.555s passed
lenOfSeqEmptyEQ data()[150] 3.367s passed
lenOfSeqSingletonEQ data()[151] 3.368s passed
lenOfSeqConcatEQ data()[152] 3.353s passed
lenOfSeqSubEQ data()[153] 3.370s passed
lenOfSeqReverseEQ data()[154] 3.369s passed
getOfSeqDefEQ data()[155] 3.350s passed
lenOfSeqDefEQ data()[156] 3.366s passed
seqConcatWithSeqEmpty1 data()[157] 3.364s passed
seqConcatWithSeqEmpty2 data()[158] 3.351s passed
seqReverseOfSeqEmpty data()[159] 3.367s passed
div_one data()[15] 3.430s passed
subSeqComplete data()[160] 3.368s passed
subSeqTailR data()[161] 3.376s passed
subSeqTailL data()[162] 3.356s passed
subSeqTailEQR data()[163] 3.363s passed
subSeqTailEQL data()[164] 3.369s passed
seqDef_split data()[165] 3.385s passed
seqDef_induction_upper data()[166] 3.385s passed
seqDef_induction_upper_concrete data()[167] 3.362s passed
seqDef_induction_lower data()[168] 3.379s passed
seqDef_induction_lower_concrete data()[169] 3.378s passed
jdiv_one data()[16] 3.419s passed
seqDef_split_in_three data()[170] 3.409s passed
seqDef_empty data()[171] 3.375s passed
seqDef_one_summand data()[172] 3.375s passed
seqDef_lower_equals_upper data()[173] 3.378s passed
seqDefOfSeq data()[174] 3.377s passed
seqSelfDefinitionEQ2 data()[175] 3.354s passed
indexOfSeqSingleton data()[176] 3.361s passed
indexOfSeqConcatFirst data()[177] 3.380s passed
indexOfSeqConcatSecond data()[178] 3.377s passed
indexOfSeqSub data()[179] 3.377s passed
div_zero data()[17] 3.459s passed
lenOfArray2seq data()[180] 3.379s passed
getAnyOfArray2seq data()[181] 3.374s passed
getOfArray2seq data()[182] 3.375s passed
getAnyOfNPermInv data()[183] 3.368s passed
seqNPermRange data()[184] 3.412s passed
seqPermTrans data()[185] 3.419s passed
seqPermRefl data()[186] 3.382s passed
seqPermSplit data()[187] 3.373s passed
seqNPermRight data()[188] 3.445s passed
seqPermFromSwap data()[189] 3.404s passed
divResZero1 data()[18] 3.409s passed
seqPermTransAlt0 data()[190] 3.383s passed
seqPermTransAlt1 data()[191] 3.378s passed
seqPermTransAlt2 data()[192] 3.364s passed
seqPermTransAlt3 data()[193] 3.382s passed
seqPermForall data()[194] 3.465s passed
seqPermExists data()[195] 3.432s passed
schiffl_lemma_2 data()[196] 21.883s passed
schiffl_thm_1 data()[197] 4.129s passed
eqSameSeq data()[198] 3.502s passed
divResZero2 data()[19] 3.397s passed
eqTermCut data()[1] 4.235s passed
divResOne1 data()[20] 3.410s passed
divResOne2 data()[21] 3.424s passed
div_cancel1 data()[22] 3.434s passed
div_cancel2 data()[23] 3.403s passed
divAddMultDenom data()[24] 3.423s passed
divMinus data()[25] 3.460s passed
divMinusDenom data()[26] 3.464s passed
divLeastDPos data()[27] 3.388s passed
divLeastDNeg data()[28] 3.376s passed
divGreatestDPos data()[29] 3.380s passed
equivAllRight data()[2] 3.817s passed
divGreatestDNeg data()[30] 3.369s passed
divIncreasingPos data()[31] 3.407s passed
divIncreasingNeg data()[32] 3.394s passed
jdiv_zero data()[33] 3.391s passed
jdivPulloutMinusNum data()[34] 3.388s passed
jdivPulloutMinusDenom data()[35] 3.425s passed
jdiv_uniquePosPos data()[36] 3.409s passed
jdiv_uniquePosNeg data()[37] 3.394s passed
jdiv_uniqueNegPos data()[38] 3.378s passed
jdiv_uniqueNegNeg data()[39] 3.373s passed
irrflConcrete1 data()[3] 3.589s passed
jdivMultDenom1 data()[40] 3.404s passed
jdivMultDenom2 data()[41] 3.376s passed
mod_geZero data()[42] 3.379s passed
mod_lessDenom data()[43] 3.379s passed
jmod_NumPos data()[44] 3.374s passed
jmod_NumNeg data()[45] 3.389s passed
jmod_geZero data()[46] 3.360s passed
jmodNumZero data()[47] 3.380s passed
jmod_pulloutminusNum data()[48] 3.381s passed
jmod_pulloutminusDenom data()[49] 3.375s passed
irrflConcrete2 data()[4] 3.578s passed
jmodUnique1 data()[50] 3.441s passed
jmodUnique2 data()[51] 3.417s passed
intDivRem data()[52] 3.352s passed
jmodjmod data()[53] 3.392s passed
jmodDivisible data()[54] 3.394s passed
jmodDivisibleRep data()[55] 3.354s passed
jdivAddMultDenom data()[56] 3.478s passed
jmodAltZero data()[57] 3.357s passed
jmodAddMultDenomZero data()[58] 3.385s passed
polyDiv_zero data()[59] 3.352s passed
cancel_gtPos data()[5] 3.527s passed
polyMod_ltdivDenom data()[60] 3.346s passed
bsum_empty data()[61] 3.338s passed
bsum_induction_upper data()[62] 3.336s passed
bsum_induction_lower data()[63] 3.378s passed
bsum_num_of_bounds data()[64] 3.381s passed
bsum_num_of_bounds2 data()[65] 3.365s passed
bsum_induction_upper2 data()[66] 3.364s passed
bsum_induction_upper_concrete data()[67] 3.396s passed
bsum_induction_upper_concrete_2 data()[68] 3.375s passed
bsum_induction_upper2_concrete data()[69] 3.346s passed
cancel_gtNeg data()[6] 3.486s passed
bsum_induction_lower_concrete data()[70] 3.361s passed
bsum_induction_lower2 data()[71] 3.360s passed
bsum_induction_lower2_concrete data()[72] 3.384s passed
bsum_positive data()[73] 3.414s passed
bsum_upper_bound data()[74] 3.378s passed
bsum_lower_bound data()[75] 3.375s passed
bsum_positive_lower_bound_element data()[76] 3.403s passed
bsum_sub_same_index data()[77] 3.411s passed
bsum_less_same_index data()[78] 3.406s passed
bsum_equal_except_one_index data()[79] 3.370s passed
moduloIntIsInInt data()[7] 3.461s passed
bsum_num_of_is_max data()[80] 3.357s passed
bsum_num_of_is_max2 data()[81] 3.392s passed
bsum_num_of_is_max3 data()[82] 3.363s passed
bsum_num_of_is_max4 data()[83] 3.360s passed
bsum_num_of_lt_max data()[84] 3.358s passed
bsum_num_of_lt_max2 data()[85] 3.376s passed
bsum_num_of_lt_max3 data()[86] 3.394s passed
bsum_num_of_lt_max4 data()[87] 3.363s passed
bsum_num_of_gt0 data()[88] 3.360s passed
bsum_num_of_gt0_alt data()[89] 3.381s passed
moduloLongIsInLong data()[8] 3.472s passed
bsum_add_concrete data()[90] 3.377s passed
bprod_all_positive data()[91] 3.350s passed
bprod_split data()[92] 3.343s passed
powConcrete0 data()[93] 3.355s passed
powConcrete1 data()[94] 3.357s passed
powSplitFactor data()[95] 3.372s passed
powAdd data()[96] 3.362s passed
powMono data()[97] 3.364s passed
powMonoConcrete data()[98] 3.340s passed
powMonoConcreteRight data()[99] 3.359s passed
moduloShortIsInShort data()[9] 3.432s passed

Standard output

571        INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src/test/resources/testcase/dummyTrue.key 
595        DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 8.69ms 
834        INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
851        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)

1753       DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for Meta 
1756       DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for Meta 
1760       DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for Meta 
1760       DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for Meta 
3110       DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for JavaBigintExpression 
8533       DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 7.7s 
8617       INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof dummyTrue.key 
8653       DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 33.4ns 
8669       INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/firstOrder/Taclet_eqTermCut.proof 
8671       DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 1.58ms 
8677       INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
11781      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.1s 
11783      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: eqTermCut 
12864      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: eqTermCut 
12893      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 20.83ms 
12906      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/firstOrder/Taclet_equivAllRight.proof 
12906      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 149.3ns 
12908      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
15723      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.81s 
15730      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: equivAllRight 
16707      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: equivAllRight 
16720      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 9.43ms 
16723      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_irrflConcrete1.proof 
16724      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 400.11ns 
16725      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
19455      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.73s 
19455      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: irrflConcrete1 
20305      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: irrflConcrete1 
20310      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.48ms 
20312      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_irrflConcrete2.proof 
20312      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 141.5ns 
20313      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
22977      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.66s 
22977      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: irrflConcrete2 
23882      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: irrflConcrete2 
23887      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.38ms 
23891      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_cancel_gtPos.proof 
23892      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 507.61ns 
23893      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
26518      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.62s 
26518      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: cancel_gtPos 
27376      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: cancel_gtPos 
27414      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 34.02ms 
27419      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_cancel_gtNeg.proof 
27419      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 415.41ns 
27420      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
30030      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.61s 
30031      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: cancel_gtNeg 
30885      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: cancel_gtNeg 
30903      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 14.44ms 
30906      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intRulesIgnoringOF/Taclet_moduloIntIsInInt.proof 
30907      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 371.61ns 
30908      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
33519      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.61s 
33520      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: moduloIntIsInInt 
34355      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: moduloIntIsInInt 
34363      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.46ms 
34368      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intRulesIgnoringOF/Taclet_moduloLongIsInLong.proof 
34369      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 481.31ns 
34371      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
36970      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.6s 
36971      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: moduloLongIsInLong 
37835      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: moduloLongIsInLong 
37838      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 618.11ns 
37841      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intRulesIgnoringOF/Taclet_moduloShortIsInShort.proof 
37841      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 344.61ns 
37842      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
40413      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.57s 
40414      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: moduloShortIsInShort 
41268      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: moduloShortIsInShort 
41270      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 589.11ns 
41272      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intRulesIgnoringOF/Taclet_moduloByteIsInByte.proof 
41272      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 100.4ns 
41273      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
43835      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.56s 
43836      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: moduloByteIsInByte 
44678      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: moduloByteIsInByte 
44681      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 653.51ns 
44682      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intRulesIgnoringOF/Taclet_moduloCharIsInChar.proof 
44683      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 103.1ns 
44683      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
47246      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.56s 
47246      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: moduloCharIsInChar 
48086      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: moduloCharIsInChar 
48089      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 625.41ns 
48091      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_div_unique1.proof 
48091      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 111.5ns 
48092      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
50703      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.61s 
50703      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: div_unique1 
51523      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: div_unique1 
51558      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 31.79ms 
51560      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_div_unique2.proof 
51560      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 140.4ns 
51561      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
54162      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.6s 
54162      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: div_unique2 
55004      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: div_unique2 
55034      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 25.77ms 
55037      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_div_exists.proof 
55038      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 139.2ns 
55040      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
57620      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.58s 
57621      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: div_exists 
58471      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: div_exists 
58590      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 110.88ms 
58592      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_div_one.proof 
58592      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 135.1ns 
58593      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
61169      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.58s 
61170      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: div_one 
62015      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: div_one 
62020      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.88ms 
62022      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdiv_one.proof 
62022      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 178.5ns 
62023      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
64611      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.59s 
64612      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdiv_one 
65436      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdiv_one 
65439      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.16ms 
65443      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_div_zero.proof 
65443      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 315.5ns 
65444      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
68024      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.58s 
68024      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: div_zero 
68862      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: div_zero 
68899      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 32.45ms 
68900      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divResZero1.proof 
68900      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 110.4ns 
68901      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
71454      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.55s 
71454      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divResZero1 
72296      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divResZero1 
72308      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 9.38ms 
72310      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divResZero2.proof 
72310      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 114.9ns 
72311      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
74855      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.54s 
74855      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divResZero2 
75694      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divResZero2 
75705      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 8.64ms 
75707      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divResOne1.proof 
75707      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 130.4ns 
75708      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
78267      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.56s 
78267      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divResOne1 
79103      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divResOne1 
79116      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 9.64ms 
79118      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divResOne2.proof 
79118      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 152.9ns 
79119      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
81714      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.59s 
81714      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divResOne2 
82527      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divResOne2 
82539      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 9.48ms 
82541      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_div_cancel1.proof 
82541      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 107.6ns 
82542      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
85104      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.56s 
85104      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: div_cancel1 
85949      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: div_cancel1 
85973      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 17.53ms 
85976      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_div_cancel2.proof 
85976      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 345.81ns 
85977      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
88535      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.56s 
88535      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: div_cancel2 
89373      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: div_cancel2 
89376      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.32ms 
89377      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divAddMultDenom.proof 
89377      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 110.5ns 
89378      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
91931      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.55s 
91931      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divAddMultDenom 
92768      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divAddMultDenom 
92799      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 25.6ms 
92802      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divMinus.proof 
92802      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 358.21ns 
92803      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
95397      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.59s 
95397      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divMinus 
96211      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divMinus 
96259      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 41.51ms 
96262      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divMinusDenom.proof 
96263      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 359.5ns 
96264      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
98858      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.59s 
98858      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divMinusDenom 
99694      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divMinusDenom 
99724      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 25.13ms 
99726      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divLeastDPos.proof 
99726      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 119.1ns 
99727      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
102271     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.54s 
102273     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divLeastDPos 
103105     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divLeastDPos 
103112     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.71ms 
103113     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divLeastDNeg.proof 
103114     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 99.1ns 
103114     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
105642     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.53s 
105642     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divLeastDNeg 
106475     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divLeastDNeg 
106487     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 9.06ms 
106489     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divGreatestDPos.proof 
106489     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 114.7ns 
106490     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
109018     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.53s 
109019     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divGreatestDPos 
109853     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divGreatestDPos 
109868     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 10.97ms 
109869     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divGreatestDNeg.proof 
109870     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 120.9ns 
109870     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
112421     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.55s 
112421     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divGreatestDNeg 
113230     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divGreatestDNeg 
113237     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.64ms 
113238     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divIncreasingPos.proof 
113239     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 113ns 
113239     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
115793     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.55s 
115793     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divIncreasingPos 
116636     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divIncreasingPos 
116645     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.98ms 
116646     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divIncreasingNeg.proof 
116646     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 100.7ns 
116647     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
119197     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.55s 
119198     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divIncreasingNeg 
120030     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divIncreasingNeg 
120038     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 5.18ms 
120041     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdiv_zero.proof 
120041     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 238.5ns 
120042     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
122578     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.54s 
122578     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdiv_zero 
123419     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdiv_zero 
123429     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 7.15ms 
123435     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdivPulloutMinusNum.proof 
123435     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 323.8ns 
123436     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
126004     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.57s 
126004     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdivPulloutMinusNum 
126813     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdivPulloutMinusNum 
126822     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 6.68ms 
126823     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdivPulloutMinusDenom.proof 
126823     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 111.9ns 
126824     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
129376     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.55s 
129378     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdivPulloutMinusDenom 
130190     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdivPulloutMinusDenom 
130245     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 46.19ms 
130249     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdiv_uniquePosPos.proof 
130250     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 309.5ns 
130252     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
132803     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.55s 
132804     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdiv_uniquePosPos 
133639     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdiv_uniquePosPos 
133656     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 14.65ms 
133658     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdiv_uniquePosNeg.proof 
133658     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 87.8ns 
133667     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
136199     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.53s 
136199     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdiv_uniquePosNeg 
137037     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdiv_uniquePosNeg 
137050     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 10.99ms 
137052     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdiv_uniqueNegPos.proof 
137052     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 112.9ns 
137053     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
139578     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.53s 
139578     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdiv_uniqueNegPos 
140414     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdiv_uniqueNegPos 
140428     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 11.16ms 
140430     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdiv_uniqueNegNeg.proof 
140430     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 95.1ns 
140431     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
142982     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.55s 
142982     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdiv_uniqueNegNeg 
143789     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdiv_uniqueNegNeg 
143802     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 9.98ms 
143803     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdivMultDenom1.proof 
143803     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 96ns 
143804     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
146345     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.54s 
146345     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdivMultDenom1 
147177     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdivMultDenom1 
147205     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 24.01ms 
147207     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdivMultDenom2.proof 
147207     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 91.2ns 
147208     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
149750     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.54s 
149750     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdivMultDenom2 
150579     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdivMultDenom2 
150582     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 888.21ns 
150583     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_mod_geZero.proof 
150583     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 71.1ns 
150584     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
153101     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.52s 
153101     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: mod_geZero 
153956     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: mod_geZero 
153960     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.76ms 
153961     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_mod_lessDenom.proof 
153961     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 87.8ns 
153962     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
156500     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.54s 
156500     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: mod_lessDenom 
157333     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: mod_lessDenom 
157339     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.1ms 
157341     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmod_NumPos.proof 
157341     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 98ns 
157342     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
159894     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.55s 
159894     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmod_NumPos 
160707     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmod_NumPos 
160714     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.45ms 
160715     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmod_NumNeg.proof 
160715     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 96.8ns 
160716     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
163257     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.54s 
163257     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmod_NumNeg 
164088     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmod_NumNeg 
164103     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 11.8ms 
164104     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmod_geZero.proof 
164104     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 90.3ns 
164105     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
166624     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.52s 
166624     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmod_geZero 
167456     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmod_geZero 
167462     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.35ms 
167464     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmodNumZero.proof 
167464     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 75.3ns 
167464     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
169986     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.52s 
169986     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmodNumZero 
170838     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmodNumZero 
170841     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.88ms 
170844     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmod_pulloutminusNum.proof 
170844     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 92.8ns 
170845     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
173412     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.57s 
173412     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmod_pulloutminusNum 
174220     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmod_pulloutminusNum 
174223     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.34ms 
174224     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmod_pulloutminusDenom.proof 
174225     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 74.4ns 
174225     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
176765     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.54s 
176765     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmod_pulloutminusDenom 
177594     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmod_pulloutminusDenom 
177598     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.36ms 
177600     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmodUnique1.proof 
177600     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 271.8ns 
177601     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
180123     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.52s 
180124     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmodUnique1 
180975     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmodUnique1 
181038     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 55.46ms 
181042     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmodUnique2.proof 
181043     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 837.81ns 
181044     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
183561     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.52s 
183562     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmodUnique2 
184393     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmodUnique2 
184457     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 55.54ms 
184459     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_intDivRem.proof 
184459     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 103.4ns 
184460     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
186973     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.51s 
186973     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: intDivRem 
187806     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: intDivRem 
187809     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.28ms 
187811     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmodjmod.proof 
187812     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 276.2ns 
187813     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
190361     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.55s 
190362     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmodjmod 
191168     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmodjmod 
191201     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 28.81ms 
191203     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmodDivisible.proof 
191204     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 335.7ns 
191205     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
193748     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.54s 
193748     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmodDivisible 
194575     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmodDivisible 
194596     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 17.3ms 
194597     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmodDivisibleRep.proof 
194597     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 80.4ns 
194598     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
197111     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.51s 
197111     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmodDivisibleRep 
197946     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmodDivisibleRep 
197949     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 999.81ns 
197953     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdivAddMultDenom.proof 
197954     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 265.7ns 
197955     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
200470     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.52s 
200471     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdivAddMultDenom 
201301     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdivAddMultDenom 
201429     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 118.02ms 
201431     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmodAltZero.proof 
201431     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 85.8ns 
201432     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
203973     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.54s 
203973     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmodAltZero 
204778     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmodAltZero 
204787     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 6.51ms 
204788     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmodAddMultDenomZero.proof 
204788     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 135.3ns 
204789     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
207339     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.55s 
207339     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmodAddMultDenomZero 
208166     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmodAddMultDenomZero 
208171     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.13ms 
208173     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_polyDiv_zero.proof 
208173     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 64.8ns 
208173     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
210683     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.51s 
210683     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: polyDiv_zero 
211509     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: polyDiv_zero 
211523     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 11.8ms 
211524     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_polyMod_ltdivDenom.proof 
211524     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 74.7ns 
211525     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
214032     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.51s 
214033     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: polyMod_ltdivDenom 
214858     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: polyMod_ltdivDenom 
214869     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.96ms 
214870     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_empty.proof 
214870     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 81.1ns 
214871     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
217370     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.5s 
217370     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_empty 
218204     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_empty 
218207     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.3ms 
218208     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_induction_upper.proof 
218208     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 100.2ns 
218209     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
220734     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.53s 
220734     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_upper 
221539     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_induction_upper 
221543     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.01ms 
221544     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_induction_lower.proof 
221544     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 62.7ns 
221545     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
224079     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.53s 
224079     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_lower 
224907     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_induction_lower 
224921     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 12.15ms 
224923     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_bounds.proof 
224923     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 74.2ns 
224924     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
227452     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.53s 
227452     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_bounds 
228287     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_bounds 
228302     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 11.81ms 
228303     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_bounds2.proof 
228303     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 69.1ns 
228304     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
230823     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.52s 
230823     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_bounds2 
231655     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_bounds2 
231667     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 9.33ms 
231669     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_induction_upper2.proof 
231669     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 79.8ns 
231669     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
234215     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.55s 
234215     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_upper2 
235027     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_induction_upper2 
235031     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.36ms 
235033     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_induction_upper_concrete.proof 
235033     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 80.1ns 
235034     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
237588     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.55s 
237588     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_upper_concrete 
238423     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_induction_upper_concrete 
238426     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.39ms 
238432     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_induction_upper_concrete_2.proof 
238432     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 332.11ns 
238433     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
240968     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.54s 
240968     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_upper_concrete_2 
241798     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_induction_upper_concrete_2 
241803     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.87ms 
241804     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_induction_upper2_concrete.proof 
241804     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 75.2ns 
241805     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
244318     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.51s 
244318     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_upper2_concrete 
245146     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_induction_upper2_concrete 
245149     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 895.11ns 
245150     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_induction_lower_concrete.proof 
245150     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 71.3ns 
245151     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
247674     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.52s 
247674     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_lower_concrete 
248506     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_induction_lower_concrete 
248509     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 515.41ns 
248511     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_induction_lower2.proof 
248511     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 238.4ns 
248512     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
251056     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.54s 
251056     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_lower2 
251866     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_induction_lower2 
251869     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.76ms 
251870     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_induction_lower2_concrete.proof 
251871     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 94ns 
251871     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
254422     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.55s 
254423     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_lower2_concrete 
255251     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_induction_lower2_concrete 
255253     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 748.91ns 
255254     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_positive.proof 
255254     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 51.6ns 
255255     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
257776     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.52s 
257777     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_positive 
258613     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_positive 
258667     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 50.82ms 
258670     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_upper_bound.proof 
258670     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 229.9ns 
258671     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
261184     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.51s 
261184     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_upper_bound 
262014     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_upper_bound 
262044     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 27.74ms 
262048     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_lower_bound.proof 
262048     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 217.8ns 
262049     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
264570     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.52s 
264570     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_lower_bound 
265400     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_lower_bound 
265421     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 17.96ms 
265422     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_positive_lower_bound_element.proof 
265422     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 89ns 
265423     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
267987     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.56s 
267987     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_positive_lower_bound_element 
268795     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_positive_lower_bound_element 
268824     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 24.52ms 
268826     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_sub_same_index.proof 
268826     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 90.5ns 
268827     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
271381     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.55s 
271382     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_sub_same_index 
272211     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_sub_same_index 
272235     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 20.14ms 
272237     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_less_same_index.proof 
272237     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 240.8ns 
272238     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
274770     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.53s 
274770     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_less_same_index 
275607     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_less_same_index 
275641     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 29.78ms 
275642     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_equal_except_one_index.proof 
275642     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 69.2ns 
275643     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
278166     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.52s 
278166     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_equal_except_one_index 
278994     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_equal_except_one_index 
279012     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 14.31ms 
279013     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_is_max.proof 
279013     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 73.3ns 
279014     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
281549     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.54s 
281549     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_is_max 
282355     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_is_max 
282368     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 10.25ms 
282370     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_is_max2.proof 
282370     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 82.5ns 
282370     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
284910     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.54s 
284910     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_is_max2 
285743     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_is_max2 
285760     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 14.83ms 
285763     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_is_max3.proof 
285763     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 224.4ns 
285764     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
288282     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.52s 
288282     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_is_max3 
289112     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_is_max3 
289124     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 9.97ms 
289125     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_is_max4.proof 
289125     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 68.1ns 
289126     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
291633     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.51s 
291633     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_is_max4 
292468     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_is_max4 
292484     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 13.23ms 
292486     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_lt_max.proof 
292486     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 164.5ns 
292487     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
295023     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.54s 
295023     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_lt_max 
295828     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_lt_max 
295843     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 12.55ms 
295844     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_lt_max2.proof 
295844     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 75.3ns 
295845     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
298388     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.54s 
298388     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_lt_max2 
299202     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_lt_max2 
299218     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 13.46ms 
299220     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_lt_max3.proof 
299220     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 58.3ns 
299221     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
301761     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.54s 
301761     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_lt_max3 
302591     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_lt_max3 
302612     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 17.67ms 
302614     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_lt_max4.proof 
302615     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 200.6ns 
302615     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
305134     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.52s 
305135     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_lt_max4 
305962     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_lt_max4 
305976     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 10.69ms 
305977     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_gt0.proof 
305977     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 61.4ns 
305978     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
308493     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.52s 
308493     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_gt0 
309320     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_gt0 
309335     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 13.09ms 
309337     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_gt0_alt.proof 
309337     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 69.7ns 
309337     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
311893     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.56s 
311894     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_gt0_alt 
312701     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_gt0_alt 
312717     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 13.13ms 
312718     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_add_concrete.proof 
312718     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 66.5ns 
312719     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
315262     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.54s 
315262     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_add_concrete 
316087     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_add_concrete 
316093     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.62ms 
316094     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bprod/Taclet_bprod_all_positive.proof 
316094     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 52ns 
316095     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
318607     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.51s 
318607     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bprod_all_positive 
319432     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bprod_all_positive 
319443     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 8.4ms 
319445     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bprod/Taclet_bprod_split.proof 
319445     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 60.9ns 
319445     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
321951     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.51s 
321951     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bprod_split 
322782     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bprod_split 
322786     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.61ms 
322787     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powConcrete0.proof 
322787     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 66.3ns 
322788     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
325307     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.52s 
325307     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powConcrete0 
326138     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powConcrete0 
326141     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.45ms 
326143     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powConcrete1.proof 
326143     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 69.4ns 
326143     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
328680     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.54s 
328680     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powConcrete1 
329496     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powConcrete1 
329499     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 791.81ns 
329500     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powSplitFactor.proof 
329500     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 55.2ns 
329500     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
332030     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.53s 
332030     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powSplitFactor 
332861     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powSplitFactor 
332870     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.46ms 
332872     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powAdd.proof 
332873     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 413.61ns 
332874     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
335397     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.52s 
335397     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powAdd 
336227     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powAdd 
336233     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.23ms 
336235     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powMono.proof 
336235     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 199ns 
336236     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
338755     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.52s 
338755     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powMono 
339587     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powMono 
339597     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 7.18ms 
339599     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powMonoConcrete.proof 
339599     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 194.3ns 
339599     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
342127     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.53s 
342127     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powMonoConcrete 
342933     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powMonoConcrete 
342936     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.59ms 
342937     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powMonoConcreteRight.proof 
342937     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 51.9ns 
342938     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
345466     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.53s 
345466     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powMonoConcreteRight 
346294     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powMonoConcreteRight 
346296     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 457.01ns 
346297     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powPositive.proof 
346297     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 63.8ns 
346298     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
348818     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.52s 
348818     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powPositive 
349649     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powPositive 
349653     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.84ms 
349655     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powPositiveConcrete.proof 
349655     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 66.4ns 
349655     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
352171     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.52s 
352171     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powPositiveConcrete 
353001     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powPositiveConcrete 
353003     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 606.21ns 
353004     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powGeq1Concrete.proof 
353004     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 52.7ns 
353005     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
355514     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.51s 
355514     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powGeq1Concrete 
356344     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powGeq1Concrete 
356346     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 500.21ns 
356348     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_pow2InIntLower.proof 
356348     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 54.7ns 
356348     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
358885     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.54s 
358885     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: pow2InIntLower 
359690     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: pow2InIntLower 
359692     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 488.31ns 
359693     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_pow2InIntUpper.proof 
359694     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 63.8ns 
359694     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
362223     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.53s 
362223     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: pow2InIntUpper 
363052     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: pow2InIntUpper 
363058     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.92ms 
363059     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logSelfConcrete.proof 
363059     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 56.5ns 
363060     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
365577     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.52s 
365577     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logSelfConcrete 
366405     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logSelfConcrete 
366412     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.64ms 
366413     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_log1Concrete.proof 
366413     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 55.8ns 
366414     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
368921     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.51s 
368921     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: log1Concrete 
369752     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: log1Concrete 
369755     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.47ms 
369756     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logProduct.proof 
369756     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 63.8ns 
369757     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
372283     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.53s 
372283     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logProduct 
373088     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logProduct 
373093     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.25ms 
373094     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logTimesBaseConcrete.proof 
373094     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 51ns 
373095     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
375624     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.53s 
375625     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logTimesBaseConcrete 
376435     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logTimesBaseConcrete 
376439     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.95ms 
376440     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logProdIdentity.proof 
376440     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 82.6ns 
376441     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
378966     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.53s 
378966     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logProdIdentity 
379795     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logProdIdentity 
379811     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 13.27ms 
379812     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logProdIdentityConcrete.proof 
379812     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 65.6ns 
379813     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
382325     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.51s 
382326     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logProdIdentityConcrete 
383155     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logProdIdentityConcrete 
383158     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.45ms 
383159     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logPowIdentity.proof 
383159     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 66.9ns 
383161     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
385668     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.51s 
385668     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logPowIdentity 
386497     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logPowIdentity 
386500     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 928.31ns 
386501     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logPowIdentityConcrete.proof 
386501     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 54.4ns 
386502     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
389037     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.53s 
389037     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logPowIdentityConcrete 
389848     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logPowIdentityConcrete 
389851     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.52ms 
389852     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logPositive.proof 
389852     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 62.1ns 
389853     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
392384     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.53s 
392385     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logPositive 
393212     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logPositive 
393225     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 10.18ms 
393227     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logPositiveConcrete.proof 
393227     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 197.6ns 
393228     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
395732     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.5s 
395732     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logPositiveConcrete 
396559     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logPositiveConcrete 
396563     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 428.81ns 
396565     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logMono.proof 
396565     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 64.9ns 
396565     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
399071     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.51s 
399071     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logMono 
399895     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logMono 
399920     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 21.28ms 
399922     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logMonoConcrete.proof 
399922     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 73.5ns 
399922     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
402458     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.54s 
402459     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logMonoConcrete 
403265     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logMonoConcrete 
403268     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.57ms 
403269     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powLogLess.proof 
403269     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 52ns 
403270     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
405797     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.53s 
405797     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powLogLess 
406626     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powLogLess 
406640     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 12.03ms 
406642     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powLogMore2.proof 
406642     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 67.8ns 
406642     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
409161     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.52s 
409161     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powLogMore2 
409999     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powLogMore2 
410013     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 10.9ms 
410014     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logLessThanPow.proof 
410014     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 62.7ns 
410015     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
412523     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.51s 
412523     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logLessThanPow 
413351     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logLessThanPow 
413368     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 14.42ms 
413370     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logLessThanPowConcrete.proof 
413370     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 70.8ns 
413370     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
415898     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.53s 
415898     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logLessThanPowConcrete 
416706     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logLessThanPowConcrete 
416708     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 563.81ns 
416710     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logSqueeze.proof 
416710     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 55.4ns 
416710     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
419243     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.53s 
419243     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logSqueeze 
420071     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logSqueeze 
420076     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.12ms 
420077     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/booleanRules/Taclet_ifthenelse_equals.proof 
420077     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 53.5ns 
420078     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
422588     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.51s 
422588     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: ifthenelse_equals 
423421     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: ifthenelse_equals 
423425     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.42ms 
423426     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/booleanRules/Taclet_ifthenelse_equals_1.proof 
423426     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 64.4ns 
423427     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
425955     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.53s 
425955     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: ifthenelse_equals_1 
426769     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: ifthenelse_equals_1 
426772     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 792.01ns 
426773     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/booleanRules/Taclet_ifthenelse_equals_2.proof 
426773     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 54.8ns 
426774     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
429309     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.54s 
429309     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: ifthenelse_equals_2 
430141     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: ifthenelse_equals_2 
430143     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 725.61ns 
430144     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/locSet/Taclet_disjointWithSingleton1.proof 
430144     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 53.8ns 
430145     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
432676     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.53s 
432676     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: disjointWithSingleton1 
433517     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: disjointWithSingleton1 
433520     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.22ms 
433522     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/locSet/Taclet_disjointWithSingleton2.proof 
433523     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 225.5ns 
433523     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
436053     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.53s 
436053     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: disjointWithSingleton2 
436868     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: disjointWithSingleton2 
436870     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.23ms 
436872     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/locSet/Taclet_disjointArrayRanges.proof 
436872     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 57.7ns 
436872     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
439400     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.53s 
439401     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: disjointArrayRanges 
440236     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: disjointArrayRanges 
440250     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 5.48ms 
440251     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/locSet/Taclet_disjointArrayRangeAllFields1.proof 
440251     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 62.3ns 
440252     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
442760     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.51s 
442760     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: disjointArrayRangeAllFields1 
443599     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: disjointArrayRangeAllFields1 
443605     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.4ms 
443607     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/locSet/Taclet_disjointArrayRangeAllFields2.proof 
443607     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 66.9ns 
443607     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
446137     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.53s 
446137     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: disjointArrayRangeAllFields2 
446974     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: disjointArrayRangeAllFields2 
446980     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.06ms 
446982     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqSelfDefinition.proof 
446982     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 73.7ns 
446983     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
449491     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.51s 
449491     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqSelfDefinition 
450333     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqSelfDefinition 
450340     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.73ms 
450341     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqOutsideValue.proof 
450341     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 102ns 
450342     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
452872     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.53s 
452872     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqOutsideValue 
453692     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqOutsideValue 
453696     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.98ms 
453697     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_castedGetAny.proof 
453697     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 65.4ns 
453698     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
456219     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.52s 
456219     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: castedGetAny 
457061     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: castedGetAny 
457065     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.25ms 
457066     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqGetAlphaCast.proof 
457066     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 51.9ns 
457066     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
459572     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.51s 
459572     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqGetAlphaCast 
460412     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqGetAlphaCast 
460414     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 641.31ns 
460415     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqSingleton.proof 
460416     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 51.1ns 
460416     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.52s 
462940     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqSingleton 
463781     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqSingleton 
463783     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 937.11ns 
463784     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqSingletonConcrete.proof 
463785     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 70.7ns 
463785     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
466290     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.5s 
466290     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqSingletonConcrete 
467137     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqSingletonConcrete 
467139     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 769.81ns 
467140     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqConcat.proof 
467141     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 63.5ns 
467141     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
469683     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.54s 
469683     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqConcat 
470526     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqConcat 
470534     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 5.96ms 
470535     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqSub.proof 
470535     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 59ns 
470536     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
473044     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.51s 
473045     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqSub 
473890     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqSub 
473893     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.16ms 
473894     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqReverse.proof 
473894     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 66.4ns 
473895     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
476418     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.52s 
476418     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqReverse 
477243     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqReverse 
477250     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 5.16ms 
477252     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqEmpty.proof 
477252     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 195.9ns 
477253     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
479787     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.53s 
479788     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqEmpty 
480629     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqEmpty 
480632     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 703.11ns 
480633     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqSingleton.proof 
480633     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 58.6ns 
480634     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
483159     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.53s 
483160     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqSingleton 
483980     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqSingleton 
483982     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 552.01ns 
483983     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqConcat.proof 
483983     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 60.7ns 
483984     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
486518     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.53s 
486518     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqConcat 
487360     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqConcat 
487363     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.29ms 
487364     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqSub.proof 
487364     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 76.4ns 
487365     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
489892     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.53s 
489892     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqSub 
490713     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqSub 
490715     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 743.71ns 
490716     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqReverse.proof 
490716     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 56.4ns 
490717     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
493242     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.52s 
493242     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqReverse 
494081     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqReverse 
494084     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 933.61ns 
494085     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_equalityToSeqGetAndSeqLenLeft.proof 
494085     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 58.3ns 
494085     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
496607     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.52s 
496607     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: equalityToSeqGetAndSeqLenLeft 
497448     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: equalityToSeqGetAndSeqLenLeft 
497451     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 907.91ns 
497452     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_equalityToSeqGetAndSeqLenRight.proof 
497452     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 61.7ns 
497453     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
499960     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.51s 
499960     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: equalityToSeqGetAndSeqLenRight 
500800     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: equalityToSeqGetAndSeqLenRight 
500803     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.96ms 
500805     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqSingletonEQ.proof 
500805     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 49.5ns 
500805     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
503345     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.54s 
503345     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqSingletonEQ 
504188     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqSingletonEQ 
504191     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 829.01ns 
504192     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqConcatEQ.proof 
504192     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 59.8ns 
504193     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
506695     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.5s 
506695     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqConcatEQ 
507536     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqConcatEQ 
507544     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 6.08ms 
507545     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqSubEQ.proof 
507545     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 51.7ns 
507546     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
510069     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.52s 
510069     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqSubEQ 
510910     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqSubEQ 
510912     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 484.41ns 
510913     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqReverseEQ.proof 
510913     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 59.5ns 
510914     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
513438     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.52s 
513438     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqReverseEQ 
514259     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqReverseEQ 
514264     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.47ms 
514266     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqEmptyEQ.proof 
514266     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 49.2ns 
514266     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
516789     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.52s 
516789     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqEmptyEQ 
517629     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqEmptyEQ 
517631     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 797.01ns 
517633     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqSingletonEQ.proof 
517633     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 46.5ns 
517633     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
520158     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.52s 
520158     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqSingletonEQ 
520998     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqSingletonEQ 
521000     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 596.41ns 
521001     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqConcatEQ.proof 
521001     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 60.8ns 
521001     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
523507     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.51s 
523507     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqConcatEQ 
524349     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqConcatEQ 
524352     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.75ms 
524353     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqSubEQ.proof 
524353     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 61.9ns 
524354     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
526878     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.52s 
526878     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqSubEQ 
527720     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqSubEQ 
527723     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 951.81ns 
527724     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqReverseEQ.proof 
527725     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 117.2ns 
527725     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
530247     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.52s 
530247     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqReverseEQ 
531089     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqReverseEQ 
531092     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.06ms 
531093     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqDefEQ.proof 
531093     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 59.5ns 
531094     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
533598     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.5s 
533598     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqDefEQ 
534439     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqDefEQ 
534442     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 894.91ns 
534443     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqDefEQ.proof 
534443     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 48.3ns 
534443     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
536963     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.52s 
536963     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqDefEQ 
537804     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqDefEQ 
537808     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.88ms 
537809     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqConcatWithSeqEmpty1.proof 
537809     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 62.2ns 
537810     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
540326     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.52s 
540326     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqConcatWithSeqEmpty1 
541165     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqConcatWithSeqEmpty1 
541171     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.94ms 
541173     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqConcatWithSeqEmpty2.proof 
541173     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 55.7ns 
541173     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
543692     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.52s 
543693     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqConcatWithSeqEmpty2 
544515     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqConcatWithSeqEmpty2 
544522     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 5.19ms 
544523     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqReverseOfSeqEmpty.proof 
544523     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 60.2ns 
544524     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
547042     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.52s 
547042     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqReverseOfSeqEmpty 
547884     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqReverseOfSeqEmpty 
547889     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.79ms 
547891     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_subSeqComplete.proof 
547891     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 47.9ns 
547891     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
550413     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.52s 
550413     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: subSeqComplete 
551252     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: subSeqComplete 
551258     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.81ms 
551259     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_subSeqTailR.proof 
551259     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 50.2ns 
551260     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
553783     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.52s 
553783     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: subSeqTailR 
554624     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: subSeqTailR 
554633     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 7.17ms 
554634     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_subSeqTailL.proof 
554634     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 63.5ns 
554635     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
557139     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.5s 
557139     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: subSeqTailL 
557980     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: subSeqTailL 
557989     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 7.37ms 
557990     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_subSeqTailEQR.proof 
557990     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 76.9ns 
557991     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
560505     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.51s 
560506     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: subSeqTailEQR 
561344     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: subSeqTailEQR 
561353     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 6.78ms 
561354     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_subSeqTailEQL.proof 
561354     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 62.1ns 
561355     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
563875     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.52s 
563875     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: subSeqTailEQL 
564715     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: subSeqTailEQL 
564722     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.53ms 
564723     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDef_split.proof 
564723     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 60ns 
564724     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
567245     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.52s 
567246     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_split 
568087     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDef_split 
568106     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 15.96ms 
568107     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDef_induction_upper.proof 
568107     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 54.8ns 
568108     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
570629     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.52s 
570630     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_induction_upper 
571471     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDef_induction_upper 
571491     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 17.23ms 
571493     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDef_induction_upper_concrete.proof 
571493     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 57.7ns 
571493     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
573994     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.5s 
573995     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_induction_upper_concrete 
574835     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDef_induction_upper_concrete 
574853     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 15.27ms 
574855     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDef_induction_lower.proof 
574855     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 65.3ns 
574855     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
577374     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.52s 
577374     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_induction_lower 
578215     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDef_induction_lower 
578232     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 14.18ms 
578233     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDef_induction_lower_concrete.proof 
578233     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 64.6ns 
578234     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
580752     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.52s 
580752     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_induction_lower_concrete 
581592     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDef_induction_lower_concrete 
581610     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 14.71ms 
581611     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDef_split_in_three.proof 
581612     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 57.1ns 
581612     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
584133     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.52s 
584133     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_split_in_three 
584974     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDef_split_in_three 
585019     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 38.09ms 
585020     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDef_empty.proof 
585020     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 66ns 
585021     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
587547     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.53s 
587547     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_empty 
588390     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDef_empty 
588394     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.61ms 
588396     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDef_one_summand.proof 
588396     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 50.2ns 
588396     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
590921     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.52s 
590921     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_one_summand 
591764     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDef_one_summand 
591769     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.98ms 
591771     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDef_lower_equals_upper.proof 
591771     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 235.1ns 
591772     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
594301     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.53s 
594301     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_lower_equals_upper 
595145     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDef_lower_equals_upper 
595148     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.79ms 
595149     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDefOfSeq.proof 
595149     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 60.8ns 
595150     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
597671     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.52s 
597671     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDefOfSeq 
598513     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDefOfSeq 
598525     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 9.19ms 
598526     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqSelfDefinitionEQ2.proof 
598526     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 64.5ns 
598527     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
601051     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.52s 
601052     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqSelfDefinitionEQ2 
601872     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqSelfDefinitionEQ2 
601878     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.86ms 
601879     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_indexOfSeqSingleton.proof 
601879     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 51.1ns 
601880     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
604395     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.51s 
604395     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: indexOfSeqSingleton 
605236     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: indexOfSeqSingleton 
605239     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.34ms 
605240     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_indexOfSeqConcatFirst.proof 
605241     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 62.1ns 
605241     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
607766     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.53s 
607767     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: indexOfSeqConcatFirst 
608610     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: indexOfSeqConcatFirst 
608619     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 7.04ms 
608621     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_indexOfSeqConcatSecond.proof 
608621     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 63.6ns 
608621     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
611145     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.52s 
611145     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: indexOfSeqConcatSecond 
611987     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: indexOfSeqConcatSecond 
611996     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 7.51ms 
611998     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_indexOfSeqSub.proof 
611998     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 64.3ns 
611998     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
614520     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.52s 
614520     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: indexOfSeqSub 
615361     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: indexOfSeqSub 
615374     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 9.79ms 
615375     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfArray2seq.proof 
615375     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 52.9ns 
615376     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
617905     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.53s 
617905     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfArray2seq 
618747     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfArray2seq 
618752     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 943.71ns 
618753     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getAnyOfArray2seq.proof 
618753     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 54.1ns 
618754     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
621272     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.52s 
621272     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getAnyOfArray2seq 
622123     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getAnyOfArray2seq 
622126     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.56ms 
622127     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfArray2seq.proof 
622127     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 65.2ns 
622128     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
624654     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.53s 
624654     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfArray2seq 
625496     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfArray2seq 
625501     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.9ms 
625502     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_getAnyOfNPermInv.proof 
625502     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 58.8ns 
625503     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
628020     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.52s 
628020     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getAnyOfNPermInv 
628865     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getAnyOfNPermInv 
628869     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.88ms 
628871     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqNPermRange.proof 
628871     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 58.7ns 
628871     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
631398     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.53s 
631398     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqNPermRange 
632242     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqNPermRange 
632281     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 33.92ms 
632282     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermTrans.proof 
632282     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 68.7ns 
632283     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
634829     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.55s 
634830     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermTrans 
635684     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermTrans 
635700     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 13.72ms 
635702     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermRefl.proof 
635702     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 66.1ns 
635702     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
638229     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.53s 
638229     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermRefl 
639072     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermRefl 
639082     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 8.41ms 
639084     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermSplit.proof 
639084     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 64.9ns 
639084     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
641605     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.52s 
641605     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermSplit 
642453     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermSplit 
642455     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 235.6ns 
642457     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqNPermRight.proof 
642458     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 64.1ns 
642459     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
644985     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.53s 
644985     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqNPermRight 
645828     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqNPermRight 
645901     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 63.37ms 
645902     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermFromSwap.proof 
645902     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 60.5ns 
645903     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
648425     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.52s 
648425     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermFromSwap 
649270     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermFromSwap 
649305     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 30.76ms 
649309     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermTransAlt0.proof 
649310     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 1.73ms 
649311     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
651844     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.53s 
651844     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermTransAlt0 
652688     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermTransAlt0 
652690     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 229.3ns 
652692     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermTransAlt1.proof 
652692     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 51.6ns 
652692     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
655212     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.52s 
655212     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermTransAlt1 
656066     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermTransAlt1 
656068     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 198.7ns 
656069     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermTransAlt2.proof 
656069     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 60.9ns 
656070     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
658606     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.54s 
658606     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermTransAlt2 
659431     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermTransAlt2 
659433     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 201.6ns 
659434     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermTransAlt3.proof 
659434     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 48.5ns 
659435     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
661970     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.54s 
661970     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermTransAlt3 
662813     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermTransAlt3 
662814     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 342.81ns 
662815     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermForall.proof 
662816     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 59.9ns 
662816     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
665333     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.52s 
665333     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermForall 
666178     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermForall 
666272     INFO  Test worker     d.u.i.k.s.SMTFocusResults Analyzing unsat core: (L_1 L_3 L_4) 
666279     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 99.01ms 
666281     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermExists.proof 
666282     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 208ns 
666283     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
668822     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.54s 
668822     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermExists 
669665     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermExists 
669710     INFO  Test worker     d.u.i.k.s.SMTFocusResults Analyzing unsat core: (L_1 L_3 L_5 L_6 L_7) 
669712     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 44.25ms 
669713     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm2/Taclet_schiffl_lemma_2.proof 
669713     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 65.4ns 
669714     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
672239     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.53s 
672240     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: schiffl_lemma_2 
673084     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: schiffl_lemma_2 
673086     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3ns 
673118     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [1] goal: 0, source line: 49, command: 'macro split-prop' 
673169     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [2] goal: 3, source line: 50, command: 'rule allRight' 
673182     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [3] goal: 4, source line: 51, command: 'rule allRight' 
673188     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [4] goal: 5, source line: 52, command: 'macro split-prop' 
673202     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [5] goal: 11, source line: 53, command: 'rule 'seqPermDefLeft'' 
673203     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [6] goal: 12, source line: 54, command: 'rule 'andLeft'' 
673204     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [7] goal: 13, source line: 55, command: 'rule 'exLeft'' 
673205     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [8] goal: 14, source line: 56, command: 'macro split-prop' 
673212     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [9] goal: 16, source line: 57, command: 'rule  seqNPermRange' 
673214     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [10] goal: 17, source line: 59, command: 'instantiate var=iv with='v_x_0' occ=1' 
673217     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [11] goal: 18, source line: 60, command: 'rule impLeft' 
673220     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [12] goal: 19, source line: 61, command: 'tryclose branch' 
673446     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [13] goal: 20, source line: 62, command: 'rule andLeft' 
673447     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [14] goal: 97, source line: 63, command: 'rule andLeft' 
673450     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [15] goal: 98, source line: 64, command: 'instantiate var=iv with='v_y_0' occ=1' 
673451     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [16] goal: 99, source line: 66, command: 'rule impLeft' 
673453     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [17] goal: 100, source line: 67, command: 'tryclose branch' 
673587     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [18] goal: 101, source line: 68, command: 'rule andLeft' 
673588     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [19] goal: 188, source line: 69, command: 'rule andLeft' 
673591     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [20] goal: 189, source line: 70, command: 'rule seqNPermDefLeft' 
673592     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [21] goal: 190, source line: 72, command: 'instantiate var=iv with='v_x_0' occ=2' 
673594     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [22] goal: 191, source line: 73, command: 'rule impLeft' 
673596     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [23] goal: 192, source line: 74, command: 'tryclose branch' 
673762     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [24] goal: 193, source line: 75, command: 'rule exLeft' 
673765     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [25] goal: 310, source line: 76, command: 'rule andLeft' 
673766     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [26] goal: 311, source line: 77, command: 'rule andLeft' 
673767     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [27] goal: 312, source line: 78, command: 'instantiate hide var=iv with='v_y_0' occ=2' 
673767     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [28] goal: 313, source line: 80, command: 'rule impLeft' 
673770     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [29] goal: 314, source line: 81, command: 'tryclose branch' 
673900     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [30] goal: 315, source line: 82, command: 'rule exLeft' 
673902     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [31] goal: 420, source line: 83, command: 'rule andLeft' 
673903     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [32] goal: 421, source line: 84, command: 'rule andLeft' 
673904     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [33] goal: 422, source line: 85, command: 'instantiate var=iv with='jv_0' occ=1' 
673904     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [34] goal: 423, source line: 87, command: 'rule impLeft' 
673905     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [35] goal: 424, source line: 88, command: 'tryclose branch' 
673914     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [36] goal: 425, source line: 89, command: 'rule andLeft' 
673914     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [37] goal: 434, source line: 90, command: 'rule andLeft' 
673916     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [38] goal: 435, source line: 91, command: 'rule castAdd formula='s_0[jv_0] = v_x_0' occ=0' 
673917     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [39] goal: 436, source line: 92, command: 'instantiate hide var=iv with='jv_1' occ=1' 
673919     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [40] goal: 437, source line: 94, command: 'rule impLeft' 
673920     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [41] goal: 438, source line: 95, command: 'tryclose branch' 
673929     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [42] goal: 439, source line: 96, command: 'rule andLeft' 
673930     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [43] goal: 448, source line: 97, command: 'rule andLeft' 
673931     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [44] goal: 449, source line: 98, command: 'rule castAdd formula='s_0[jv_1] = v_y_0' occ=0' 
673932     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [45] goal: 450, source line: 99, command: 'instantiate var=iv  with='v_x_0'' 
673933     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [46] goal: 451, source line: 101, command: 'rule impLeft' 
673934     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [47] goal: 452, source line: 102, command: 'tryclose branch' 
674111     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [48] goal: 453, source line: 103, command: 'instantiate var=iv  with='v_y_0'' 
674113     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [49] goal: 562, source line: 105, command: 'rule impLeft' 
674114     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [50] goal: 563, source line: 106, command: 'tryclose branch' 
674236     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [51] goal: 564, source line: 107, command: 'cut 'v_x_0 = v_y_0'' 
674237     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [52] goal: 674, source line: 109, command: 'instantiate hide var='v_r' with='seqSwap(s_0,v_x_0,jv_0)'' 
674238     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [53] goal: 676, source line: 111, command: 'rule andRight' 
674240     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [54] goal: 677, source line: 113, command: 'rule andRight' 
674241     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [55] goal: 679, source line: 114, command: 'rule andRight' 
674243     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [56] goal: 681, source line: 115, command: 'rule andRight' 
674245     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [57] goal: 683, source line: 116, command: 'rule lenOfSwap' 
674251     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [58] goal: 685, source line: 117, command: 'tryclose branch' 
674254     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [59] goal: 684, source line: 118, command: 'rule seqNPermSwapNPerm' 
674260     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [60] goal: 687, source line: 120, command: 'instantiate hide var='iv' with='v_x_0' occ=1' 
674262     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [61] goal: 688, source line: 121, command: 'instantiate hide var='jv' with='jv_0'' 
674262     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [62] goal: 689, source line: 122, command: 'rule impLeft' 
674263     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [63] goal: 690, source line: 123, command: 'tryclose branch' 
674361     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [64] goal: 691, source line: 124, command: 'tryclose branch' 
674365     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [65] goal: 682, source line: 125, command: 'rule allRight' 
674366     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [66] goal: 796, source line: 127, command: 'rule impRight' 
674367     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [67] goal: 797, source line: 128, command: 'rule andLeft' 
674368     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [68] goal: 798, source line: 129, command: 'instantiate var=iv with='v_iv_0'' 
674368     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [69] goal: 799, source line: 130, command: 'rule impLeft' 
674373     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [70] goal: 800, source line: 131, command: 'tryclose branch' 
674490     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [71] goal: 801, source line: 132, command: 'rule getOfSwap' 
674491     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [72] goal: 912, source line: 133, command: 'rule ifthenelse_negated' 
674493     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [73] goal: 913, source line: 134, command: 'rule ifthenelse_split occ=0' 
674496     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [74] goal: 914, source line: 135, command: 'rule andLeft' 
674496     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [75] goal: 916, source line: 136, command: 'rule andLeft' 
674497     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [76] goal: 917, source line: 137, command: 'rule andLeft' 
674498     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [77] goal: 918, source line: 138, command: 'rule ifthenelse_split occ=0' 
674499     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [78] goal: 919, source line: 139, command: 'tryclose branch' 
674588     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [79] goal: 920, source line: 140, command: 'rule ifthenelse_split occ=0' 
674589     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [80] goal: 1011, source line: 141, command: 'tryclose branch' 
674669     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [81] goal: 1012, source line: 142, command: 'tryclose branch' 
674673     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [82] goal: 915, source line: 143, command: 'tryclose branch' 
674678     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [83] goal: 680, source line: 144, command: 'rule getOfSwap' 
674679     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [84] goal: 1099, source line: 146, command: 'rule ifthenelse_negated' 
674682     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [85] goal: 1100, source line: 147, command: 'rule ifthenelse_split occ=0' 
674683     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [86] goal: 1101, source line: 148, command: 'rule andLeft' 
674684     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [87] goal: 1103, source line: 149, command: 'rule andLeft' 
674684     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [88] goal: 1104, source line: 150, command: 'rule andLeft' 
674685     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [89] goal: 1105, source line: 151, command: 'rule ifthenelse_split occ=0' 
674685     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [90] goal: 1106, source line: 152, command: 'tryclose branch' 
674693     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [91] goal: 1107, source line: 153, command: 'tryclose branch' 
674697     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [92] goal: 1102, source line: 154, command: 'tryclose branch' 
674799     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [93] goal: 678, source line: 155, command: 'rule getOfSwap' 
674799     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [94] goal: 1225, source line: 157, command: 'rule ifthenelse_negated' 
674801     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [95] goal: 1226, source line: 158, command: 'rule ifthenelse_split occ=0' 
674802     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [96] goal: 1227, source line: 159, command: 'rule andLeft' 
674803     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [97] goal: 1229, source line: 160, command: 'rule andLeft' 
674803     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [98] goal: 1230, source line: 161, command: 'rule andLeft' 
674804     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [99] goal: 1231, source line: 162, command: 'rule ifthenelse_split occ=0' 
674805     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [100] goal: 1232, source line: 163, command: 'tryclose branch' 
674854     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [101] goal: 1233, source line: 164, command: 'tryclose branch' 
674859     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [102] goal: 1228, source line: 165, command: 'tryclose branch' 
674945     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [103] goal: 675, source line: 166, command: 'cut '(int)s_0[v_x_0] = (int)s_0[v_y_0]'' 
674946     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [104] goal: 1397, source line: 169, command: 'rule seqNPermInjective' 
674948     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [105] goal: 1399, source line: 170, command: 'instantiate hide var=iv with='v_x_0'' 
674949     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [106] goal: 1400, source line: 171, command: 'instantiate hide var=jv with='v_y_0'' 
674950     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [107] goal: 1401, source line: 172, command: 'rule impLeft' 
674951     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [108] goal: 1402, source line: 173, command: 'tryclose branch' 
675069     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [109] goal: 1403, source line: 174, command: 'tryclose branch' 
675073     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [110] goal: 1398, source line: 175, command: 'cut '(int)s_0[v_x_0] = v_x_0'' 
675075     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [111] goal: 1534, source line: 177, command: 'instantiate hide var=v_r with='seqSwap(s_0,v_y_0,jv_1)'' 
675076     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [112] goal: 1536, source line: 179, command: 'rule andRight' 
675078     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [113] goal: 1537, source line: 181, command: 'rule andRight' 
675078     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [114] goal: 1539, source line: 182, command: 'rule andRight' 
675079     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [115] goal: 1541, source line: 183, command: 'rule andRight' 
675079     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [116] goal: 1543, source line: 184, command: 'tryclose branch' 
675088     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [117] goal: 1544, source line: 185, command: 'rule seqNPermSwapNPerm' 
675093     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [118] goal: 1558, source line: 187, command: 'instantiate hide var=iv with='v_y_0'' 
675094     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [119] goal: 1559, source line: 188, command: 'instantiate hide var=jv with='jv_1'' 
675095     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [120] goal: 1560, source line: 189, command: 'tryclose branch' 
675205     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [121] goal: 1542, source line: 190, command: 'rule allRight' 
675206     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [122] goal: 1667, source line: 192, command: 'rule impRight' 
675207     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [123] goal: 1668, source line: 193, command: 'rule andLeft' 
675208     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [124] goal: 1669, source line: 194, command: 'instantiate var=iv with='v_iv_0'' 
675208     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [125] goal: 1670, source line: 195, command: 'rule impLeft' 
675209     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [126] goal: 1671, source line: 196, command: 'tryclose branch' 
675310     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [127] goal: 1672, source line: 197, command: 'rule getOfSwap' 
675311     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [128] goal: 1786, source line: 198, command: 'rule ifthenelse_negated' 
675312     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [129] goal: 1787, source line: 199, command: 'rule ifthenelse_split occ=0' 
675314     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [130] goal: 1788, source line: 200, command: 'rule andLeft' 
675314     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [131] goal: 1790, source line: 201, command: 'rule andLeft' 
675315     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [132] goal: 1791, source line: 202, command: 'rule andLeft' 
675315     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [133] goal: 1792, source line: 203, command: 'rule ifthenelse_split occ=0' 
675316     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [134] goal: 1793, source line: 204, command: 'tryclose branch' 
675393     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [135] goal: 1794, source line: 205, command: 'rule ifthenelse_split occ=0' 
675396     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [136] goal: 1885, source line: 206, command: 'tryclose branch' 
675467     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [137] goal: 1886, source line: 207, command: 'instantiate var=iv with='v_y_0'' 
675467     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [138] goal: 1968, source line: 208, command: 'rule impLeft' 
675468     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [139] goal: 1969, source line: 209, command: 'tryclose branch' 
675472     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [140] goal: 1970, source line: 210, command: 'tryclose branch' 
675475     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [141] goal: 1789, source line: 211, command: 'tryclose branch' 
675480     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [142] goal: 1540, source line: 212, command: 'tryclose branch' 
675594     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [143] goal: 1538, source line: 213, command: 'rule getOfSwap' 
675595     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [144] goal: 2097, source line: 215, command: 'rule ifthenelse_negated' 
675601     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [145] goal: 2098, source line: 216, command: 'rule ifthenelse_split occ=0' 
675602     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [146] goal: 2099, source line: 217, command: 'tryclose branch' 
675617     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [147] goal: 2100, source line: 218, command: 'tryclose branch' 
675699     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [148] goal: 1535, source line: 219, command: 'tryclose branch' 
679240     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [149] goal: 1535, source line: 221, command: 'cut  '(int)s_0[v_y_0] = v_y_0'' 
679240     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [150] goal: 4266, source line: 224, command: 'instantiate hide var=v_r with='seqSwap(s_0,v_x_0,jv_0)'' 
679244     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [151] goal: 4268, source line: 226, command: 'rule andRight' 
679245     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [152] goal: 4269, source line: 228, command: 'rule andRight' 
679246     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [153] goal: 4271, source line: 229, command: 'rule andRight' 
679246     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [154] goal: 4273, source line: 230, command: 'rule andRight' 
679247     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [155] goal: 4275, source line: 231, command: 'tryclose branch' 
679254     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [156] goal: 4276, source line: 232, command: 'rule seqNPermSwapNPerm' 
679255     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [157] goal: 4287, source line: 234, command: 'instantiate hide var=iv with='v_x_0'' 
679256     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [158] goal: 4288, source line: 235, command: 'instantiate hide var=jv with='jv_0'' 
679257     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [159] goal: 4289, source line: 236, command: 'rule impLeft' 
679257     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [160] goal: 4290, source line: 237, command: 'tryclose branch' 
679347     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [161] goal: 4291, source line: 238, command: 'tryclose branch' 
679351     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [162] goal: 4274, source line: 239, command: 'rule allRight' 
679351     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [163] goal: 4400, source line: 241, command: 'rule impRight' 
679352     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [164] goal: 4401, source line: 242, command: 'rule andLeft' 
679353     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [165] goal: 4402, source line: 243, command: 'instantiate var=iv with='v_iv_0'' 
679353     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [166] goal: 4403, source line: 244, command: 'rule impLeft' 
679354     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [167] goal: 4404, source line: 245, command: 'tryclose branch' 
679446     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [168] goal: 4405, source line: 246, command: 'rule getOfSwap' 
679446     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [169] goal: 4521, source line: 247, command: 'rule ifthenelse_negated' 
679447     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [170] goal: 4522, source line: 248, command: 'rule ifthenelse_split occ=0' 
679448     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [171] goal: 4523, source line: 249, command: 'rule andLeft' 
679449     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [172] goal: 4525, source line: 250, command: 'rule andLeft' 
679449     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [173] goal: 4526, source line: 251, command: 'rule andLeft' 
679450     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [174] goal: 4527, source line: 252, command: 'rule ifthenelse_split occ=0' 
679450     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [175] goal: 4528, source line: 253, command: 'tryclose branch' 
679524     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [176] goal: 4529, source line: 254, command: 'rule ifthenelse_split occ=0' 
679525     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [177] goal: 4622, source line: 255, command: 'tryclose branch' 
679597     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [178] goal: 4623, source line: 256, command: 'tryclose branch' 
679601     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [179] goal: 4524, source line: 257, command: 'tryclose branch' 
679605     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [180] goal: 4272, source line: 258, command: 'rule getOfSwap' 
679606     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [181] goal: 4713, source line: 260, command: 'rule ifthenelse_negated' 
679607     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [182] goal: 4714, source line: 261, command: 'rule ifthenelse_split occ=0' 
679608     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [183] goal: 4715, source line: 262, command: 'tryclose branch' 
679617     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [184] goal: 4716, source line: 263, command: 'tryclose branch' 
679695     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [185] goal: 4270, source line: 264, command: 'rule getOfSwap' 
679695     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [186] goal: 4839, source line: 266, command: 'rule ifthenelse_negated' 
679696     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [187] goal: 4840, source line: 267, command: 'rule ifthenelse_split occ=0' 
679697     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [188] goal: 4841, source line: 268, command: 'tryclose branch' 
679767     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [189] goal: 4842, source line: 269, command: 'tryclose branch' 
679776     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [190] goal: 4267, source line: 270, command: 'cut '(int)s_0[v_x_0]=v_y_0'' 
679776     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [191] goal: 4948, source line: 273, command: 'instantiate hide var=v_r with='seqSwap(seqSwap(s_0,jv_0,v_x_0),jv_0,v_y_0)'' 
679777     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [192] goal: 4950, source line: 275, command: 'rule andRight' 
679778     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [193] goal: 4951, source line: 277, command: 'rule andRight' 
679779     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [194] goal: 4953, source line: 278, command: 'rule andRight' 
679779     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [195] goal: 4955, source line: 279, command: 'rule andRight' 
679779     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [196] goal: 4957, source line: 280, command: 'tryclose branch' 
679790     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [197] goal: 4958, source line: 281, command: 'rule seqNPermSwapNPerm' 
679791     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [198] goal: 4977, source line: 283, command: 'instantiate hide var=iv with='jv_0'' 
679791     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [199] goal: 4978, source line: 284, command: 'instantiate hide var=jv with='v_x_0'' 
679792     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [200] goal: 4979, source line: 285, command: 'rule impLeft' 
679793     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [201] goal: 4980, source line: 286, command: 'tryclose branch' 
679878     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [202] goal: 4981, source line: 287, command: 'rule seqNPermSwapNPerm formula='seqNPerm(seqSwap(s_0, jv_0, v_x_0))'' 
679878     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [203] goal: 5093, source line: 288, command: 'instantiate hide var=iv with='jv_0'' 
679879     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [204] goal: 5094, source line: 289, command: 'instantiate hide var=jv with='v_y_0'' 
679880     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [205] goal: 5095, source line: 290, command: 'rule impLeft' 
679881     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [206] goal: 5096, source line: 291, command: 'tryclose branch' 
679968     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [207] goal: 5097, source line: 292, command: 'tryclose branch' 
679973     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [208] goal: 4956, source line: 293, command: 'rule allRight' 
679973     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [209] goal: 5212, source line: 295, command: 'rule impRight' 
679974     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [210] goal: 5213, source line: 296, command: 'rule andLeft' 
679974     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [211] goal: 5214, source line: 297, command: 'instantiate var=iv with='v_iv_0'' 
679975     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [212] goal: 5215, source line: 300, command: 'rule impLeft' 
679975     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [213] goal: 5216, source line: 301, command: 'tryclose branch' 
680117     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [214] goal: 5217, source line: 302, command: 'rule getOfSwap' 
680118     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [215] goal: 5337, source line: 304, command: 'rule ifthenelse_negated' 
680119     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [216] goal: 5338, source line: 305, command: 'rule ifthenelse_split occ=0' 
680120     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [217] goal: 5339, source line: 306, command: 'rule andLeft' 
680120     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [218] goal: 5341, source line: 307, command: 'rule andLeft' 
680121     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [219] goal: 5342, source line: 308, command: 'rule andLeft' 
680121     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [220] goal: 5343, source line: 309, command: 'rule ifthenelse_split occ=0' 
680122     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [221] goal: 5344, source line: 310, command: 'rule getOfSwap' 
680123     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [222] goal: 5346, source line: 311, command: 'rule ifthenelse_negated' 
680123     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [223] goal: 5347, source line: 312, command: 'rule ifthenelse_split occ=0' 
680124     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [224] goal: 5348, source line: 313, command: 'rule andLeft' 
680125     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [225] goal: 5350, source line: 314, command: 'rule andLeft' 
680125     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [226] goal: 5351, source line: 315, command: 'rule andLeft' 
680125     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [227] goal: 5352, source line: 316, command: 'rule ifthenelse_split occ=0' 
680126     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [228] goal: 5353, source line: 317, command: 'tryclose branch' 
680209     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [229] goal: 5354, source line: 318, command: 'rule ifthenelse_split occ=0' 
680210     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [230] goal: 5463, source line: 319, command: 'tryclose branch' 
680216     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [231] goal: 5464, source line: 320, command: 'tryclose branch' 
680291     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [232] goal: 5349, source line: 321, command: 'tryclose branch' 
680368     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [233] goal: 5345, source line: 322, command: 'rule ifthenelse_split' 
680369     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [234] goal: 5660, source line: 324, command: 'rule getOfSwap' 
680369     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [235] goal: 5662, source line: 325, command: 'rule ifthenelse_negated' 
680370     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [236] goal: 5663, source line: 326, command: 'rule ifthenelse_split occ=0' 
680371     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [237] goal: 5664, source line: 327, command: 'rule andLeft' 
680371     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [238] goal: 5666, source line: 328, command: 'rule andLeft' 
680372     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [239] goal: 5667, source line: 329, command: 'rule andLeft' 
680372     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [240] goal: 5668, source line: 330, command: 'rule ifthenelse_split occ=0' 
680373     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [241] goal: 5669, source line: 331, command: 'tryclose branch' 
680454     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [242] goal: 5670, source line: 332, command: 'tryclose branch' 
680460     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [243] goal: 5665, source line: 333, command: 'tryclose branch' 
680545     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [244] goal: 5661, source line: 334, command: 'rule getOfSwap' 
680546     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [245] goal: 5887, source line: 336, command: 'rule ifthenelse_negated' 
680547     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [246] goal: 5888, source line: 337, command: 'rule ifthenelse_split occ=0' 
680548     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [247] goal: 5889, source line: 338, command: 'rule andLeft' 
680548     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [248] goal: 5891, source line: 339, command: 'rule andLeft' 
680549     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [249] goal: 5892, source line: 340, command: 'rule andLeft' 
680549     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [250] goal: 5893, source line: 341, command: 'rule ifthenelse_split occ=0' 
680549     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [251] goal: 5894, source line: 342, command: 'tryclose branch' 
680554     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [252] goal: 5895, source line: 343, command: 'rule ifthenelse_split occ=0' 
680555     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [253] goal: 5897, source line: 344, command: 'tryclose branch' 
680632     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [254] goal: 5898, source line: 345, command: 'tryclose branch' 
680637     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [255] goal: 5890, source line: 346, command: 'tryclose branch' 
680642     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [256] goal: 5340, source line: 347, command: 'tryclose branch' 
680739     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [257] goal: 4954, source line: 348, command: 'rule getOfSwap' 
680740     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [258] goal: 6115, source line: 350, command: 'rule ifthenelse_negated' 
680740     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [259] goal: 6116, source line: 351, command: 'rule ifthenelse_split occ=0' 
680741     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [260] goal: 6117, source line: 352, command: 'rule andLeft' 
680742     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [261] goal: 6119, source line: 353, command: 'rule andLeft' 
680742     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [262] goal: 6120, source line: 354, command: 'rule andLeft' 
680742     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [263] goal: 6121, source line: 355, command: 'rule ifthenelse_split occ=0' 
680743     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [264] goal: 6122, source line: 356, command: 'tryclose branch' 
680796     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [265] goal: 6123, source line: 357, command: 'rule ifthenelse_split occ=0' 
680797     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [266] goal: 6193, source line: 358, command: 'rule getOfSwap' 
680797     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [267] goal: 6195, source line: 359, command: 'rule ifthenelse_negated' 
680798     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [268] goal: 6196, source line: 360, command: 'rule ifthenelse_split occ=0' 
680798     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [269] goal: 6197, source line: 361, command: 'tryclose branch' 
680804     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [270] goal: 6198, source line: 362, command: 'tryclose branch' 
680809     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [271] goal: 6194, source line: 363, command: 'tryclose branch' 
680922     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [272] goal: 6118, source line: 364, command: 'tryclose branch' 
681007     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [273] goal: 4952, source line: 365, command: 'rule getOfSwap' 
681008     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [274] goal: 6456, source line: 367, command: 'rule ifthenelse_negated' 
681009     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [275] goal: 6457, source line: 368, command: 'rule ifthenelse_split occ=0' 
681010     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [276] goal: 6458, source line: 369, command: 'tryclose branch' 
681171     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [277] goal: 6459, source line: 370, command: 'tryclose branch' 
681258     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [278] goal: 4949, source line: 371, command: 'cut 'int::seqGet(s_0, v_y_0)=v_x_0'' 
681259     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [279] goal: 6735, source line: 375, command: 'tryclose branch' 
684176     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [280] goal: 6735, source line: 378, command: 'rule seqNPermSwapNPerm' 
684180     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [281] goal: 8783, source line: 380, command: 'instantiate hide var=iv with='jv_1'' 
684181     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [282] goal: 8784, source line: 381, command: 'instantiate hide var=jv with='v_y_0'' 
684182     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [283] goal: 8785, source line: 382, command: 'rule impLeft' 
684183     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [284] goal: 8786, source line: 383, command: 'tryclose branch' 
684294     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [285] goal: 8787, source line: 384, command: 'rule seqNPermSwapNPerm formula='seqNPerm(seqSwap(s_0,jv_1,v_y_0))'' 
684294     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [286] goal: 8909, source line: 385, command: 'instantiate hide var=iv with='jv_1'' 
684295     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [287] goal: 8910, source line: 386, command: 'instantiate hide var=jv with='v_x_0'' 
684296     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [288] goal: 8911, source line: 387, command: 'rule impLeft' 
684297     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [289] goal: 8912, source line: 388, command: 'tryclose branch' 
684401     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [290] goal: 8913, source line: 389, command: 'tryclose branch' 
687241     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [291] goal: 6736, source line: 390, command: 'tryclose branch' 
690355     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [292] goal: 6736, source line: 397, command: 'rule seqNPermSwapNPerm formula='seqNPerm(s_0)'' 
690359     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [293] goal: 12633, source line: 399, command: 'instantiate hide var=iv with='v_x_0'' 
690360     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [294] goal: 12634, source line: 400, command: 'instantiate hide var=jv with='jv_0'' 
690361     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [295] goal: 12635, source line: 401, command: 'rule impLeft' 
690362     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [296] goal: 12636, source line: 402, command: 'tryclose branch' 
690474     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [297] goal: 12637, source line: 403, command: 'rule seqNPermSwapNPerm formula='seqNPerm(seqSwap(s_0,v_x_0,jv_0))'' 
690474     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [298] goal: 12757, source line: 404, command: 'instantiate hide var=iv with='v_y_0'' 
690475     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [299] goal: 12758, source line: 405, command: 'instantiate hide var=jv with='jv_1'' 
690476     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [300] goal: 12759, source line: 406, command: 'instantiate hide var=v_r with='seqSwap(seqSwap(s_0, v_x_0, jv_0), v_y_0, jv_1)' ...' 
690477     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [301] goal: 12760, source line: 407, command: 'tryclose branch' 
691595     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm2/Taclet_schiffl_thm_1.proof 
691595     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 93.3ns 
691596     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
694177     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.58s 
694178     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: schiffl_thm_1 
695046     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: schiffl_thm_1 
695048     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 7.1ns 
695048     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [1] goal: 0, source line: 50, command: 'macro split-prop' 
695058     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [2] goal: 10, source line: 51, command: 'rule schiffl_lemma_2 formula='seqPerm(f_s, f_t)'' 
695066     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [3] goal: 11, source line: 52, command: 'instantiate hide var=x with='f_x'' 
695069     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [4] goal: 12, source line: 53, command: 'instantiate hide var=y with='f_y'' 
695071     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [5] goal: 13, source line: 54, command: 'rule impLeft' 
695072     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [6] goal: 14, source line: 55, command: 'tryclose branch' 
695077     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [7] goal: 15, source line: 56, command: 'rule exLeft' 
695078     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [8] goal: 23, source line: 57, command: 'macro split-prop' 
695085     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [9] goal: 27, source line: 58, command: 'rule seqPermDef occ=1' 
695085     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [10] goal: 28, source line: 59, command: 'rule andRight' 
695088     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [11] goal: 29, source line: 60, command: 'tryclose branch' 
695099     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [12] goal: 30, source line: 61, command: 'instantiate hide var=s with='r_0'' 
695099     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [13] goal: 46, source line: 62, command: 'rule andRight' 
695101     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [14] goal: 47, source line: 63, command: 'tryclose branch' 
695149     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [15] goal: 48, source line: 64, command: 'rule allRight' 
695150     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [16] goal: 119, source line: 65, command: 'rule impRight' 
695150     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [17] goal: 120, source line: 66, command: 'instantiate hide var=iv with='iv_0'' 
695151     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [18] goal: 121, source line: 67, command: 'rule impLeft' 
695151     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [19] goal: 122, source line: 68, command: 'tryclose branch' 
695212     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [20] goal: 123, source line: 69, command: 'rule andLeft' 
695213     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [21] goal: 203, source line: 70, command: 'rule seqNPermRange' 
695213     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [22] goal: 204, source line: 71, command: 'instantiate hide var=iv with='iv_0'' 
695214     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [23] goal: 205, source line: 72, command: 'rule impLeft' 
695215     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [24] goal: 206, source line: 73, command: 'tryclose branch' 
695219     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [25] goal: 207, source line: 74, command: 'rule andLeft' 
695219     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [26] goal: 215, source line: 75, command: 'rule andLeft' 
695219     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [27] goal: 216, source line: 76, command: 'rule seqNPermRange' 
695220     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [28] goal: 217, source line: 77, command: 'instantiate hide var=iv with='f_x'' 
695221     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [29] goal: 218, source line: 78, command: 'rule impLeft' 
695221     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [30] goal: 219, source line: 79, command: 'tryclose branch' 
695299     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [31] goal: 220, source line: 80, command: 'rule andLeft' 
695300     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [32] goal: 311, source line: 81, command: 'rule andLeft' 
695300     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [33] goal: 312, source line: 82, command: 'rule seqNPermRange' 
695301     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [34] goal: 313, source line: 83, command: 'instantiate hide var=iv with='f_y'' 
695301     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [35] goal: 314, source line: 84, command: 'rule impLeft' 
695302     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [36] goal: 315, source line: 85, command: 'tryclose branch' 
695377     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [37] goal: 316, source line: 86, command: 'rule andLeft' 
695378     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [38] goal: 410, source line: 87, command: 'rule andLeft' 
695378     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [39] goal: 411, source line: 88, command: 'rule getOfSeqDef occ=0' 
695379     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [40] goal: 412, source line: 89, command: 'rule getOfSeqDef' 
695379     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [41] goal: 413, source line: 90, command: 'rule ifthenelse_split occ=0' 
695380     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [42] goal: 414, source line: 91, command: 'rule andLeft occ=0' 
695380     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [43] goal: 416, source line: 92, command: 'rule sub_zero_2 occ=0' 
695381     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [44] goal: 417, source line: 93, command: 'rule ifthenelse_split occ=2' 
695381     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [45] goal: 418, source line: 94, command: 'rule andLeft' 
695382     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [46] goal: 420, source line: 95, command: 'rule sub_zero_2 occ=0' 
695382     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [47] goal: 421, source line: 96, command: 'rule add_zero_right occ=0' 
695382     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [48] goal: 422, source line: 97, command: 'rule add_zero_right occ=0' 
695383     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [49] goal: 423, source line: 98, command: 'rule add_zero_right occ=0' 
695383     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [50] goal: 424, source line: 99, command: 'rule add_zero_right occ=0' 
695384     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [51] goal: 425, source line: 100, command: 'rule add_zero_right occ=0' 
695384     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [52] goal: 426, source line: 101, command: 'rule add_zero_right occ=0' 
695384     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [53] goal: 427, source line: 102, command: 'rule ifthenelse_split occ=0' 
695385     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [54] goal: 428, source line: 103, command: 'rule ifthenelse_split occ=0' 
695385     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [55] goal: 430, source line: 104, command: 'tryclose branch' 
695388     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [56] goal: 431, source line: 105, command: 'tryclose branch' 
695419     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [57] goal: 429, source line: 106, command: 'rule ifthenelse_split occ=0' 
695420     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [58] goal: 473, source line: 107, command: 'tryclose branch' 
695467     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [59] goal: 474, source line: 108, command: 'rule ifthenelse_split occ=0' 
695468     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [60] goal: 541, source line: 109, command: 'rule seqNPermInjective' 
695469     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [61] goal: 543, source line: 110, command: 'instantiate hide var=iv with='iv_0'' 
695470     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [62] goal: 544, source line: 111, command: 'instantiate hide var=jv with='f_y'' 
695471     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [63] goal: 545, source line: 112, command: 'rule impLeft' 
695471     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [64] goal: 546, source line: 113, command: 'tryclose branch' 
695516     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [65] goal: 547, source line: 114, command: 'tryclose branch' 
695518     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [66] goal: 542, source line: 115, command: 'rule ifthenelse_split occ=0' 
695519     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [67] goal: 606, source line: 116, command: 'rule seqNPermInjective' 
695520     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [68] goal: 608, source line: 117, command: 'instantiate hide var=iv with='iv_0'' 
695521     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [69] goal: 609, source line: 118, command: 'instantiate hide var=jv with='f_x'' 
695522     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [70] goal: 610, source line: 119, command: 'rule impLeft' 
695522     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [71] goal: 611, source line: 120, command: 'tryclose branch' 
695564     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [72] goal: 612, source line: 121, command: 'tryclose branch' 
695566     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [73] goal: 607, source line: 122, command: 'tryclose branch' 
695569     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [74] goal: 419, source line: 123, command: 'tryclose branch' 
695618     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [75] goal: 415, source line: 124, command: 'tryclose branch' 
695724     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_eqSameSeq.proof 
695725     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 83.1ns 
695725     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
698311     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.59s 
698312     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: eqSameSeq 
699210     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: eqSameSeq 
699225     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 12.02ms