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

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

tests
0

failures
0

ignored
10m50.06s

duration
100%

successful

Tests

Test Method name Duration Result
powPositive data()[100] 2.985s passed
powPositiveConcrete data()[101] 2.959s passed
powGeq1Concrete data()[102] 2.961s passed
pow2InIntLower data()[103] 3.052s passed
pow2InIntUpper data()[104] 3.060s passed
logSelfConcrete data()[105] 3.189s passed
log1Concrete data()[106] 3.142s passed
logProduct data()[107] 2.942s passed
logTimesBaseConcrete data()[108] 2.955s passed
logProdIdentity data()[109] 2.956s passed
moduloByteIsInByte data()[10] 3.446s passed
logProdIdentityConcrete data()[110] 3.006s passed
logPowIdentity data()[111] 2.978s passed
logPowIdentityConcrete data()[112] 2.961s passed
logPositive data()[113] 3.011s passed
logPositiveConcrete data()[114] 2.938s passed
logMono data()[115] 2.911s passed
logMonoConcrete data()[116] 2.940s passed
powLogLess data()[117] 2.963s passed
powLogMore2 data()[118] 3.192s passed
logLessThanPow data()[119] 3.258s passed
moduloCharIsInChar data()[11] 3.427s passed
logLessThanPowConcrete data()[120] 3.245s passed
logSqueeze data()[121] 3.430s passed
ifthenelse_equals data()[122] 3.379s passed
ifthenelse_equals_1 data()[123] 3.204s passed
ifthenelse_equals_2 data()[124] 3.249s passed
disjointWithSingleton1 data()[125] 3.434s passed
disjointWithSingleton2 data()[126] 3.312s passed
disjointArrayRanges data()[127] 3.291s passed
disjointArrayRangeAllFields1 data()[128] 3.386s passed
disjointArrayRangeAllFields2 data()[129] 3.116s passed
div_unique1 data()[12] 3.624s passed
seqSelfDefinition data()[130] 2.957s passed
seqOutsideValue data()[131] 2.959s passed
castedGetAny data()[132] 2.977s passed
seqGetAlphaCast data()[133] 3.045s passed
getOfSeqSingleton data()[134] 2.994s passed
getOfSeqSingletonConcrete data()[135] 2.941s passed
getOfSeqConcat data()[136] 3.046s passed
getOfSeqSub data()[137] 3.081s passed
getOfSeqReverse data()[138] 2.950s passed
lenOfSeqEmpty data()[139] 2.967s passed
div_unique2 data()[13] 3.540s passed
lenOfSeqSingleton data()[140] 2.971s passed
lenOfSeqConcat data()[141] 2.992s passed
lenOfSeqSub data()[142] 2.933s passed
lenOfSeqReverse data()[143] 2.968s passed
equalityToSeqGetAndSeqLenLeft data()[144] 3.152s passed
equalityToSeqGetAndSeqLenRight data()[145] 3.121s passed
getOfSeqSingletonEQ data()[146] 3.189s passed
getOfSeqConcatEQ data()[147] 3.242s passed
getOfSeqSubEQ data()[148] 3.114s passed
getOfSeqReverseEQ data()[149] 2.983s passed
div_exists data()[14] 3.563s passed
lenOfSeqEmptyEQ data()[150] 3.009s passed
lenOfSeqSingletonEQ data()[151] 2.967s passed
lenOfSeqConcatEQ data()[152] 3.003s passed
lenOfSeqSubEQ data()[153] 2.998s passed
lenOfSeqReverseEQ data()[154] 2.909s passed
getOfSeqDefEQ data()[155] 2.969s passed
lenOfSeqDefEQ data()[156] 2.998s passed
seqConcatWithSeqEmpty1 data()[157] 2.945s passed
seqConcatWithSeqEmpty2 data()[158] 2.958s passed
seqReverseOfSeqEmpty data()[159] 2.937s passed
div_one data()[15] 3.333s passed
subSeqComplete data()[160] 3.023s passed
subSeqTailR data()[161] 2.976s passed
subSeqTailL data()[162] 2.962s passed
subSeqTailEQR data()[163] 3.099s passed
subSeqTailEQL data()[164] 2.998s passed
seqDef_split data()[165] 2.953s passed
seqDef_induction_upper data()[166] 3.015s passed
seqDef_induction_upper_concrete data()[167] 3.147s passed
seqDef_induction_lower data()[168] 3.179s passed
seqDef_induction_lower_concrete data()[169] 3.067s passed
jdiv_one data()[16] 3.378s passed
seqDef_split_in_three data()[170] 3.064s passed
seqDef_empty data()[171] 3.039s passed
seqDef_one_summand data()[172] 3.042s passed
seqDef_lower_equals_upper data()[173] 2.960s passed
seqDefOfSeq data()[174] 2.977s passed
seqSelfDefinitionEQ2 data()[175] 3.132s passed
indexOfSeqSingleton data()[176] 3.169s passed
indexOfSeqConcatFirst data()[177] 3.177s passed
indexOfSeqConcatSecond data()[178] 3.445s passed
indexOfSeqSub data()[179] 3.344s passed
div_zero data()[17] 3.449s passed
lenOfArray2seq data()[180] 3.280s passed
getAnyOfArray2seq data()[181] 3.325s passed
getOfArray2seq data()[182] 3.309s passed
getAnyOfNPermInv data()[183] 3.306s passed
seqNPermRange data()[184] 3.265s passed
seqPermTrans data()[185] 3.050s passed
seqPermRefl data()[186] 2.947s passed
seqPermSplit data()[187] 3.022s passed
seqNPermRight data()[188] 2.994s passed
seqPermFromSwap data()[189] 3.010s passed
divResZero1 data()[18] 3.433s passed
seqPermTransAlt0 data()[190] 2.921s passed
seqPermTransAlt1 data()[191] 2.944s passed
seqPermTransAlt2 data()[192] 2.970s passed
seqPermTransAlt3 data()[193] 2.927s passed
seqPermForall data()[194] 3.294s passed
seqPermExists data()[195] 3.363s passed
schiffl_lemma_2 data()[196] 22.746s passed
schiffl_thm_1 data()[197] 4.298s passed
eqSameSeq data()[198] 3.416s passed
divResZero2 data()[19] 3.364s passed
eqTermCut data()[1] 3.986s passed
divResOne1 data()[20] 3.385s passed
divResOne2 data()[21] 3.388s passed
div_cancel1 data()[22] 3.382s passed
div_cancel2 data()[23] 3.347s passed
divAddMultDenom data()[24] 3.399s passed
divMinus data()[25] 3.433s passed
divMinusDenom data()[26] 3.386s passed
divLeastDPos data()[27] 3.344s passed
divLeastDNeg data()[28] 3.337s passed
divGreatestDPos data()[29] 3.390s passed
equivAllRight data()[2] 3.502s passed
divGreatestDNeg data()[30] 3.380s passed
divIncreasingPos data()[31] 3.394s passed
divIncreasingNeg data()[32] 3.435s passed
jdiv_zero data()[33] 3.396s passed
jdivPulloutMinusNum data()[34] 3.436s passed
jdivPulloutMinusDenom data()[35] 3.576s passed
jdiv_uniquePosPos data()[36] 3.492s passed
jdiv_uniquePosNeg data()[37] 3.450s passed
jdiv_uniqueNegPos data()[38] 3.355s passed
jdiv_uniqueNegNeg data()[39] 3.450s passed
irrflConcrete1 data()[3] 3.671s passed
jdivMultDenom1 data()[40] 3.407s passed
jdivMultDenom2 data()[41] 3.312s passed
mod_geZero data()[42] 3.153s passed
mod_lessDenom data()[43] 3.243s passed
jmod_NumPos data()[44] 3.265s passed
jmod_NumNeg data()[45] 3.246s passed
jmod_geZero data()[46] 3.178s passed
jmodNumZero data()[47] 3.325s passed
jmod_pulloutminusNum data()[48] 3.326s passed
jmod_pulloutminusDenom data()[49] 3.383s passed
irrflConcrete2 data()[4] 3.559s passed
jmodUnique1 data()[50] 3.384s passed
jmodUnique2 data()[51] 3.450s passed
intDivRem data()[52] 3.447s passed
jmodjmod data()[53] 3.148s passed
jmodDivisible data()[54] 3.098s passed
jmodDivisibleRep data()[55] 3.306s passed
jdivAddMultDenom data()[56] 3.330s passed
jmodAltZero data()[57] 3.026s passed
jmodAddMultDenomZero data()[58] 2.948s passed
polyDiv_zero data()[59] 3.047s passed
cancel_gtPos data()[5] 3.563s passed
polyMod_ltdivDenom data()[60] 2.970s passed
bsum_empty data()[61] 2.938s passed
bsum_induction_upper data()[62] 2.929s passed
bsum_induction_lower data()[63] 3.011s passed
bsum_num_of_bounds data()[64] 3.005s passed
bsum_num_of_bounds2 data()[65] 3.021s passed
bsum_induction_upper2 data()[66] 3.321s passed
bsum_induction_upper_concrete data()[67] 3.174s passed
bsum_induction_upper_concrete_2 data()[68] 3.262s passed
bsum_induction_upper2_concrete data()[69] 3.520s passed
cancel_gtNeg data()[6] 3.507s passed
bsum_induction_lower_concrete data()[70] 3.540s passed
bsum_induction_lower2 data()[71] 3.423s passed
bsum_induction_lower2_concrete data()[72] 3.242s passed
bsum_positive data()[73] 3.546s passed
bsum_upper_bound data()[74] 3.388s passed
bsum_lower_bound data()[75] 3.520s passed
bsum_positive_lower_bound_element data()[76] 3.301s passed
bsum_sub_same_index data()[77] 3.139s passed
bsum_less_same_index data()[78] 3.031s passed
bsum_equal_except_one_index data()[79] 2.933s passed
moduloIntIsInInt data()[7] 3.504s passed
bsum_num_of_is_max data()[80] 3.051s passed
bsum_num_of_is_max2 data()[81] 2.940s passed
bsum_num_of_is_max3 data()[82] 2.960s passed
bsum_num_of_is_max4 data()[83] 2.967s passed
bsum_num_of_lt_max data()[84] 2.986s passed
bsum_num_of_lt_max2 data()[85] 2.977s passed
bsum_num_of_lt_max3 data()[86] 3.019s passed
bsum_num_of_lt_max4 data()[87] 3.092s passed
bsum_num_of_gt0 data()[88] 2.988s passed
bsum_num_of_gt0_alt data()[89] 2.940s passed
moduloLongIsInLong data()[8] 3.618s passed
bsum_add_concrete data()[90] 2.943s passed
bprod_all_positive data()[91] 2.973s passed
bprod_split data()[92] 2.967s passed
powConcrete0 data()[93] 2.929s passed
powConcrete1 data()[94] 2.946s passed
powSplitFactor data()[95] 2.972s passed
powAdd data()[96] 2.997s passed
powMono data()[97] 3.035s passed
powMonoConcrete data()[98] 3.170s passed
powMonoConcreteRight data()[99] 3.014s passed
moduloShortIsInShort data()[9] 3.499s passed

Standard output

664        INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src/test/resources/testcase/dummyTrue.key 
690        DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 9.32ms 
946        INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
961        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)

1860       DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for Meta 
1866       DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for Meta 
1868       DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for Meta 
1869       DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for Meta 
3200       DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for JavaBigintExpression 
9163       DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 8.22s 
9238       INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof dummyTrue.key 
9276       DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 33.5ns 
9292       INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/firstOrder/Taclet_eqTermCut.proof 
9293       DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 178.61ns 
9300       INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
12213      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.91s 
12221      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: eqTermCut 
13245      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: eqTermCut 
13268      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 17.97ms 
13278      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/firstOrder/Taclet_equivAllRight.proof 
13281      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 2.45ms 
13282      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
15889      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.61s 
15890      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: equivAllRight 
16764      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: equivAllRight 
16777      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 9.52ms 
16780      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_irrflConcrete1.proof 
16781      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 134.71ns 
16782      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
19503      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.72s 
19504      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: irrflConcrete1 
20443      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: irrflConcrete1 
20449      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.73ms 
20451      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_irrflConcrete2.proof 
20451      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 122.81ns 
20453      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
23116      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.66s 
23117      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: irrflConcrete2 
23997      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: irrflConcrete2 
24008      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 6.66ms 
24015      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_cancel_gtPos.proof 
24015      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 557.84ns 
24017      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
26673      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.66s 
26674      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: cancel_gtPos 
27539      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: cancel_gtPos 
27576      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 33.96ms 
27580      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_cancel_gtNeg.proof 
27580      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 419.23ns 
27582      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
30227      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.64s 
30227      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: cancel_gtNeg 
31068      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: cancel_gtNeg 
31084      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 13.77ms 
31086      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intRulesIgnoringOF/Taclet_moduloIntIsInInt.proof 
31086      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 128.11ns 
31087      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
33738      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.65s 
33738      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: moduloIntIsInInt 
34585      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: moduloIntIsInInt 
34588      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 742.55ns 
34590      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intRulesIgnoringOF/Taclet_moduloLongIsInLong.proof 
34591      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 232.92ns 
34593      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
37328      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.73s 
37328      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: moduloLongIsInLong 
38202      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: moduloLongIsInLong 
38205      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 649.35ns 
38209      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intRulesIgnoringOF/Taclet_moduloShortIsInShort.proof 
38210      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 557.54ns 
38211      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
40848      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.64s 
40849      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: moduloShortIsInShort 
41703      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: moduloShortIsInShort 
41706      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 655.25ns 
41708      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intRulesIgnoringOF/Taclet_moduloByteIsInByte.proof 
41709      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 362.03ns 
41710      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
44300      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.59s 
44301      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: moduloByteIsInByte 
45149      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: moduloByteIsInByte 
45152      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 651.55ns 
45155      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intRulesIgnoringOF/Taclet_moduloCharIsInChar.proof 
45155      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 315.52ns 
45156      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
47722      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.57s 
47723      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: moduloCharIsInChar 
48576      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: moduloCharIsInChar 
48579      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 686.85ns 
48582      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_div_unique1.proof 
48583      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 377.33ns 
48584      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
51216      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.63s 
51216      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: div_unique1 
52135      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: div_unique1 
52203      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 55.98ms 
52214      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_div_unique2.proof 
52214      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 218.82ns 
52215      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
54825      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.61s 
54825      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: div_unique2 
55685      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: div_unique2 
55743      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 53.24ms 
55745      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_div_exists.proof 
55745      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 135.31ns 
55746      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
58271      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.53s 
58272      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: div_exists 
59142      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: div_exists 
59305      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 153.25ms 
59310      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_div_one.proof 
59310      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 433.43ns 
59311      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
61810      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.5s 
61811      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: div_one 
62637      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: div_one 
62641      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.37ms 
62643      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdiv_one.proof 
62644      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 406.33ns 
62645      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
65163      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.52s 
65164      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdiv_one 
66017      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdiv_one 
66020      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.17ms 
66022      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_div_zero.proof 
66022      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 211.82ns 
66024      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
68564      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.54s 
68566      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: div_zero 
69416      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: div_zero 
69467      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 46.02ms 
69470      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divResZero1.proof 
69471      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 134.11ns 
69471      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
72017      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.55s 
72018      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divResZero1 
72889      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divResZero1 
72902      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 9.16ms 
72904      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divResZero2.proof 
72905      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 352.53ns 
72906      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
75404      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.5s 
75405      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divResZero2 
76254      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divResZero2 
76265      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 7.87ms 
76268      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divResOne1.proof 
76268      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 352.53ns 
76270      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
78807      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.54s 
78807      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divResOne1 
79639      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divResOne1 
79651      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 9.32ms 
79653      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divResOne2.proof 
79653      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 122.01ns 
79654      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
82188      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.53s 
82189      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divResOne2 
83029      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divResOne2 
83040      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 8ms 
83041      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_div_cancel1.proof 
83041      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 134.91ns 
83042      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
85572      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.53s 
85573      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: div_cancel1 
86404      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: div_cancel1 
86422      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 13.68ms 
86423      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_div_cancel2.proof 
86423      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 115.71ns 
86424      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
88933      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.51s 
88934      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: div_cancel2 
89765      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: div_cancel2 
89769      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.34ms 
89770      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divAddMultDenom.proof 
89770      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 107.91ns 
89771      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
92268      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.5s 
92268      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divAddMultDenom 
93135      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divAddMultDenom 
93167      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 26.08ms 
93169      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divMinus.proof 
93169      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 124.21ns 
93170      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
95717      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.55s 
95717      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divMinus 
96556      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divMinus 
96599      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 36.64ms 
96602      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divMinusDenom.proof 
96602      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 362.53ns 
96604      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
99142      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.54s 
99142      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divMinusDenom 
99955      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divMinusDenom 
99986      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 26.29ms 
99988      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divLeastDPos.proof 
99988      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 132.61ns 
99989      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
102509     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.52s 
102510     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divLeastDPos 
103321     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divLeastDPos 
103329     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.44ms 
103333     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divLeastDNeg.proof 
103334     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 728.65ns 
103335     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
105838     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.5s 
105838     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divLeastDNeg 
106655     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divLeastDNeg 
106667     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 9.32ms 
106670     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divGreatestDPos.proof 
106671     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 368.53ns 
106672     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
109238     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.57s 
109239     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divGreatestDPos 
110039     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divGreatestDPos 
110053     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 11.08ms 
110062     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divGreatestDNeg.proof 
110065     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 3.54ms 
110066     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
112621     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.55s 
112622     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divGreatestDNeg 
113432     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divGreatestDNeg 
113439     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 5.21ms 
113440     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divIncreasingPos.proof 
113440     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 98.01ns 
113441     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
116003     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.56s 
116003     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divIncreasingPos 
116825     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divIncreasingPos 
116833     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.7ms 
116835     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divIncreasingNeg.proof 
116835     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 323.12ns 
116837     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
119463     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.63s 
119463     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divIncreasingNeg 
120261     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divIncreasingNeg 
120268     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.59ms 
120271     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdiv_zero.proof 
120271     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 328.22ns 
120272     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
122853     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.58s 
122854     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdiv_zero 
123661     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdiv_zero 
123664     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.46ms 
123666     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdivPulloutMinusNum.proof 
123666     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 109.71ns 
123667     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
126222     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.56s 
126223     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdivPulloutMinusNum 
127078     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdivPulloutMinusNum 
127100     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 19.23ms 
127102     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdivPulloutMinusDenom.proof 
127103     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 320.92ns 
127107     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
129752     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.64s 
129754     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdivPulloutMinusDenom 
130637     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdivPulloutMinusDenom 
130675     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 32.25ms 
130678     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdiv_uniquePosPos.proof 
130679     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 343.02ns 
130680     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
133283     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.6s 
133284     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdiv_uniquePosPos 
134152     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdiv_uniquePosPos 
134169     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 12.78ms 
134174     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdiv_uniquePosNeg.proof 
134175     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 424.43ns 
134176     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
136772     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.6s 
136772     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdiv_uniquePosNeg 
137605     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdiv_uniquePosNeg 
137619     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 11.25ms 
137620     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdiv_uniqueNegPos.proof 
137621     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 99.41ns 
137621     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
140130     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.51s 
140130     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdiv_uniqueNegPos 
140952     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdiv_uniqueNegPos 
140974     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 17.56ms 
140976     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdiv_uniqueNegNeg.proof 
140976     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 178.01ns 
140977     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
143571     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.59s 
143571     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdiv_uniqueNegNeg 
144409     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdiv_uniqueNegNeg 
144424     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 11.98ms 
144425     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdivMultDenom1.proof 
144425     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 125.11ns 
144426     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
146942     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.52s 
146943     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdivMultDenom1 
147794     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdivMultDenom1 
147831     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 30.68ms 
147834     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdivMultDenom2.proof 
147834     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 350.33ns 
147835     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
150309     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.47s 
150309     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdivMultDenom2 
151140     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdivMultDenom2 
151143     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 988.47ns 
151144     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_mod_geZero.proof 
151144     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 67.11ns 
151145     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
153509     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.36s 
153510     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: mod_geZero 
154293     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: mod_geZero 
154297     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.93ms 
154298     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_mod_lessDenom.proof 
154298     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 74.11ns 
154299     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
156746     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.45s 
156747     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: mod_lessDenom 
157532     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: mod_lessDenom 
157539     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.74ms 
157541     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmod_NumPos.proof 
157541     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 210.82ns 
157542     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
159975     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.43s 
159976     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmod_NumPos 
160793     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmod_NumPos 
160804     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 9ms 
160806     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmod_NumNeg.proof 
160806     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 104.01ns 
160807     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
163231     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.42s 
163231     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmod_NumNeg 
164036     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmod_NumNeg 
164051     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 11.69ms 
164052     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmod_geZero.proof 
164052     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 109.01ns 
164053     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
166412     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.36s 
166412     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmod_geZero 
167221     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmod_geZero 
167228     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.66ms 
167229     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmodNumZero.proof 
167229     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 68.7ns 
167230     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
169728     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.5s 
169728     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmodNumZero 
170551     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmodNumZero 
170553     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 979.97ns 
170554     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmod_pulloutminusNum.proof 
170554     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 71ns 
170555     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
173066     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.51s 
173066     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmod_pulloutminusNum 
173876     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmod_pulloutminusNum 
173879     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.38ms 
173881     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmod_pulloutminusDenom.proof 
173881     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 70.2ns 
173882     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
176398     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.52s 
176398     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmod_pulloutminusDenom 
177259     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmod_pulloutminusDenom 
177263     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.8ms 
177264     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmodUnique1.proof 
177264     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 69.5ns 
177265     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
179777     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.51s 
179777     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmodUnique1 
180594     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmodUnique1 
180646     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 44.85ms 
180648     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmodUnique2.proof 
180648     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 194.41ns 
180649     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
183176     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.53s 
183176     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmodUnique2 
184019     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmodUnique2 
184096     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 66.63ms 
184102     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_intDivRem.proof 
184102     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 116.61ns 
184103     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
186750     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.65s 
186751     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: intDivRem 
187546     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: intDivRem 
187549     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.04ms 
187550     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmodjmod.proof 
187550     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 185.61ns 
187551     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
189930     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.38s 
189930     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmodjmod 
190669     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmodjmod 
190696     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 23.53ms 
190698     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmodDivisible.proof 
190698     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 315.22ns 
190699     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
192973     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.27s 
192974     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmodDivisible 
193772     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmodDivisible 
193794     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 18.43ms 
193796     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmodDivisibleRep.proof 
193796     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 165.61ns 
193797     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
196286     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.49s 
196286     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmodDivisibleRep 
197098     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmodDivisibleRep 
197100     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.08ms 
197102     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdivAddMultDenom.proof 
197102     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 80.41ns 
197103     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
199554     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.45s 
199554     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdivAddMultDenom 
200306     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdivAddMultDenom 
200430     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 113.06ms 
200431     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmodAltZero.proof 
200431     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 84.11ns 
200432     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
202684     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.25s 
202684     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmodAltZero 
203449     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmodAltZero 
203456     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 6.17ms 
203458     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmodAddMultDenomZero.proof 
203458     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 86.31ns 
203459     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
205664     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.21s 
205664     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmodAddMultDenomZero 
206399     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmodAddMultDenomZero 
206405     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.95ms 
206406     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_polyDiv_zero.proof 
206406     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 66.11ns 
206407     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
208700     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.29s 
208700     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: polyDiv_zero 
209437     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: polyDiv_zero 
209451     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 11.58ms 
209452     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_polyMod_ltdivDenom.proof 
209452     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 74.71ns 
209453     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
211673     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.22s 
211673     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: polyMod_ltdivDenom 
212410     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: polyMod_ltdivDenom 
212421     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.64ms 
212423     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_empty.proof 
212423     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 127.21ns 
212424     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
214630     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.21s 
214631     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_empty 
215357     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_empty 
215360     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.23ms 
215361     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_induction_upper.proof 
215361     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 55.51ns 
215362     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
217531     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.17s 
217531     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_upper 
218286     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_induction_upper 
218290     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.15ms 
218293     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_induction_lower.proof 
218294     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 262.12ns 
218295     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
220559     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.26s 
220559     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_lower 
221287     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_induction_lower 
221303     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 9.58ms 
221305     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_bounds.proof 
221305     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 210.62ns 
221306     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
223545     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.24s 
223545     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_bounds 
224297     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_bounds 
224308     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 8.05ms 
224311     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_bounds2.proof 
224321     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 10.22ms 
224322     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
226584     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.26s 
226584     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_bounds2 
227319     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_bounds2 
227330     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 8.22ms 
227331     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_induction_upper2.proof 
227331     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 83.81ns 
227332     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
229811     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.48s 
229811     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_upper2 
230645     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_induction_upper2 
230651     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.62ms 
230654     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_induction_upper_concrete.proof 
230654     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 240.02ns 
230655     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
232986     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.33s 
232986     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_upper_concrete 
233822     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_induction_upper_concrete 
233825     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.37ms 
233827     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_induction_upper_concrete_2.proof 
233828     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 261.62ns 
233829     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
236241     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.41s 
236241     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_upper_concrete_2 
237083     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_induction_upper_concrete_2 
237087     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.82ms 
237089     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_induction_upper2_concrete.proof 
237089     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 75.21ns 
237090     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
239716     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.63s 
239716     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_upper2_concrete 
240604     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_induction_upper2_concrete 
240607     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 862.96ns 
240609     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_induction_lower_concrete.proof 
240610     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 271.62ns 
240610     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
243284     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.67s 
243284     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_lower_concrete 
244144     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_induction_lower_concrete 
244147     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 509.54ns 
244149     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_induction_lower2.proof 
244149     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 256.12ns 
244150     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
246758     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.61s 
246758     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_lower2 
247567     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_induction_lower2 
247570     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.81ms 
247572     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_induction_lower2_concrete.proof 
247572     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 77.71ns 
247572     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
249984     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.41s 
249985     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_lower2_concrete 
250810     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_induction_lower2_concrete 
250813     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 906.57ns 
250815     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_positive.proof 
250815     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 277.02ns 
250816     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
253471     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.66s 
253471     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_positive 
254323     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_positive 
254359     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 33.42ms 
254360     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_upper_bound.proof 
254360     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 78.81ns 
254361     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
256896     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.53s 
256896     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_upper_bound 
257719     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_upper_bound 
257746     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 23.67ms 
257748     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_lower_bound.proof 
257748     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 78.51ns 
257749     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
260414     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.67s 
260414     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_lower_bound 
261244     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_lower_bound 
261267     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 19.44ms 
261268     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_positive_lower_bound_element.proof 
261268     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 71.11ns 
261269     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
263764     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.49s 
263764     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_positive_lower_bound_element 
264537     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_positive_lower_bound_element 
264567     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 25.68ms 
264568     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_sub_same_index.proof 
264568     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 83.61ns 
264569     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
266903     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.33s 
266903     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_sub_same_index 
267688     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_sub_same_index 
267706     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 14.39ms 
267708     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_less_same_index.proof 
267709     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 237.12ns 
267713     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
269959     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.25s 
269959     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_less_same_index 
270705     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_less_same_index 
270738     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 28.4ms 
270739     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_equal_except_one_index.proof 
270739     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 94.81ns 
270740     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
272949     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.21s 
272949     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_equal_except_one_index 
273655     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_equal_except_one_index 
273671     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 13.12ms 
273673     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_is_max.proof 
273673     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 93.11ns 
273674     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
275922     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.25s 
275923     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_is_max 
276680     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_is_max 
276722     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 38.77ms 
276723     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_is_max2.proof 
276724     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 66.91ns 
276724     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
278906     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.18s 
278906     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_is_max2 
279648     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_is_max2 
279663     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 11.67ms 
279665     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_is_max3.proof 
279665     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 186.41ns 
279666     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
281882     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.22s 
281882     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_is_max3 
282611     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_is_max3 
282624     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 10.28ms 
282625     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_is_max4.proof 
282625     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 74ns 
282626     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
284836     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.21s 
284836     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_is_max4 
285576     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_is_max4 
285592     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 13.04ms 
285593     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_lt_max.proof 
285593     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 68.7ns 
285594     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
287804     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.21s 
287805     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_lt_max 
288560     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_lt_max 
288577     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 13.61ms 
288578     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_lt_max2.proof 
288578     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 98.31ns 
288579     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
290789     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.21s 
290790     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_lt_max2 
291539     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_lt_max2 
291555     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 12.46ms 
291556     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_lt_max3.proof 
291556     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 66.81ns 
291557     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
293797     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.24s 
293797     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_lt_max3 
294558     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_lt_max3 
294574     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 12.78ms 
294577     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_lt_max4.proof 
294577     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 257.72ns 
294578     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
296882     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.3s 
296882     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_lt_max4 
297652     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_lt_max4 
297667     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 11.97ms 
297668     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_gt0.proof 
297668     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 73.61ns 
297669     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
299901     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.23s 
299901     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_gt0 
300639     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_gt0 
300655     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 12.72ms 
300656     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_gt0_alt.proof 
300656     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 63.8ns 
300657     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
302844     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.19s 
302844     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_gt0_alt 
303576     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_gt0_alt 
303594     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 14.44ms 
303595     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_add_concrete.proof 
303595     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 75.01ns 
303596     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
305797     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.2s 
305798     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_add_concrete 
306528     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_add_concrete 
306537     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 6.41ms 
306539     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bprod/Taclet_bprod_all_positive.proof 
306540     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 277.62ns 
306541     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
308744     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.2s 
308744     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bprod_all_positive 
309500     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bprod_all_positive 
309511     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 8.86ms 
309512     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bprod/Taclet_bprod_split.proof 
309512     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 52.1ns 
309513     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
311725     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.21s 
311725     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bprod_split 
312475     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bprod_split 
312478     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.96ms 
312479     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powConcrete0.proof 
312479     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 55ns 
312480     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
314677     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.2s 
314678     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powConcrete0 
315405     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powConcrete0 
315407     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 491.04ns 
315409     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powConcrete1.proof 
315409     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 173.71ns 
315410     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
317607     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.2s 
317607     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powConcrete1 
318352     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powConcrete1 
318354     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 671.85ns 
318355     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powSplitFactor.proof 
318355     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 68.2ns 
318355     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
320569     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.21s 
320570     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powSplitFactor 
321321     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powSplitFactor 
321325     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.8ms 
321326     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powAdd.proof 
321327     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 84.61ns 
321327     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
323567     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.24s 
323567     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powAdd 
324318     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powAdd 
324323     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.69ms 
324324     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powMono.proof 
324324     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 50.5ns 
324324     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
326550     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.23s 
326550     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powMono 
327347     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powMono 
327358     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 8.06ms 
327359     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powMonoConcrete.proof 
327359     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 69.61ns 
327360     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
329748     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.39s 
329748     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powMonoConcrete 
330524     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powMonoConcrete 
330528     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.62ms 
330529     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powMonoConcreteRight.proof 
330529     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 57.5ns 
330530     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
332836     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.31s 
332836     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powMonoConcreteRight 
333540     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powMonoConcreteRight 
333542     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 445.13ns 
333543     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powPositive.proof 
333543     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 71ns 
333543     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
335773     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.23s 
335773     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powPositive 
336521     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powPositive 
336527     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.62ms 
336528     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powPositiveConcrete.proof 
336528     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 62.1ns 
336529     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
338775     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.25s 
338775     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powPositiveConcrete 
339483     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powPositiveConcrete 
339485     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 517.04ns 
339486     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powGeq1Concrete.proof 
339486     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 86.61ns 
339487     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
341732     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.24s 
341732     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powGeq1Concrete 
342445     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powGeq1Concrete 
342447     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 456.43ns 
342448     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_pow2InIntLower.proof 
342448     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 69.7ns 
342449     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
344727     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.28s 
344728     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: pow2InIntLower 
345497     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: pow2InIntLower 
345499     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 547.04ns 
345501     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_pow2InIntUpper.proof 
345501     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 69.11ns 
345501     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
347797     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.3s 
347797     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: pow2InIntUpper 
348556     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: pow2InIntUpper 
348559     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.67ms 
348561     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logSelfConcrete.proof 
348561     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 55.3ns 
348561     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
350928     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.37s 
350928     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logSelfConcrete 
351741     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logSelfConcrete 
351748     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.64ms 
351750     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_log1Concrete.proof 
351750     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 53.1ns 
351750     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
354141     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.39s 
354142     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: log1Concrete 
354888     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: log1Concrete 
354891     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.38ms 
354892     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logProduct.proof 
354892     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 49ns 
354893     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
357097     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.2s 
357097     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logProduct 
357828     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logProduct 
357833     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.31ms 
357834     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logTimesBaseConcrete.proof 
357834     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 62.9ns 
357835     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
360041     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.21s 
360042     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logTimesBaseConcrete 
360783     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logTimesBaseConcrete 
360787     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.31ms 
360788     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logProdIdentity.proof 
360788     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 66.31ns 
360789     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
363004     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.21s 
363004     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logProdIdentity 
363733     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logProdIdentity 
363744     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 9.29ms 
363745     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logProdIdentityConcrete.proof 
363745     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 69.31ns 
363746     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
365968     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.22s 
365969     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logProdIdentityConcrete 
366742     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logProdIdentityConcrete 
366750     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 7.1ms 
366753     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logPowIdentity.proof 
366753     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 313.52ns 
366754     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
368971     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.22s 
368971     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logPowIdentity 
369724     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logPowIdentity 
369729     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.55ms 
369730     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logPowIdentityConcrete.proof 
369730     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 47.6ns 
369731     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
371959     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.23s 
371959     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logPowIdentityConcrete 
372686     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logPowIdentityConcrete 
372689     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.62ms 
372690     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logPositive.proof 
372690     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 59.51ns 
372691     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
374951     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.26s 
374951     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logPositive 
375688     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logPositive 
375700     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 9.9ms 
375701     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logPositiveConcrete.proof 
375701     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 71.5ns 
375702     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
377905     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.2s 
377905     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logPositiveConcrete 
378633     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logPositiveConcrete 
378638     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 356.83ns 
378640     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logMono.proof 
378640     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 77.91ns 
378641     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
380815     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.17s 
380815     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logMono 
381524     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logMono 
381549     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 20.79ms 
381550     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logMonoConcrete.proof 
381550     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 61.01ns 
381551     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
383759     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.21s 
383759     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logMonoConcrete 
384487     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logMonoConcrete 
384490     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.58ms 
384491     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powLogLess.proof 
384491     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 48.6ns 
384492     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
386686     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.19s 
386686     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powLogLess 
387440     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powLogLess 
387454     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 10.83ms 
387455     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powLogMore2.proof 
387455     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 59.8ns 
387456     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
389777     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.32s 
389778     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powLogMore2 
390631     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powLogMore2 
390646     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 11.61ms 
390647     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logLessThanPow.proof 
390647     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 71.11ns 
390648     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
393090     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.44s 
393090     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logLessThanPow 
393886     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logLessThanPow 
393903     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 14.24ms 
393905     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logLessThanPowConcrete.proof 
393905     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 67.11ns 
393905     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
396310     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.4s 
396310     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logLessThanPowConcrete 
397146     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logLessThanPowConcrete 
397149     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 524.34ns 
397150     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logSqueeze.proof 
397150     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 55.6ns 
397151     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
399683     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.53s 
399683     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logSqueeze 
400573     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logSqueeze 
400579     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.42ms 
400580     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/booleanRules/Taclet_ifthenelse_equals.proof 
400580     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 53.7ns 
400583     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
403158     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.58s 
403158     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: ifthenelse_equals 
403954     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: ifthenelse_equals 
403957     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.43ms 
403958     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/booleanRules/Taclet_ifthenelse_equals_1.proof 
403958     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 60.01ns 
403959     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
406445     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.49s 
406445     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: ifthenelse_equals_1 
407159     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: ifthenelse_equals_1 
407161     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 751.65ns 
407162     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/booleanRules/Taclet_ifthenelse_equals_2.proof 
407162     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 47.7ns 
407163     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
409528     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.36s 
409528     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: ifthenelse_equals_2 
410408     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: ifthenelse_equals_2 
410411     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 779.76ns 
410412     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/locSet/Taclet_disjointWithSingleton1.proof 
410412     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 60.8ns 
410413     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
413037     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.62s 
413037     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: disjointWithSingleton1 
413841     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: disjointWithSingleton1 
413844     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.25ms 
413845     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/locSet/Taclet_disjointWithSingleton2.proof 
413845     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 66.81ns 
413846     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
416339     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.49s 
416339     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: disjointWithSingleton2 
417153     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: disjointWithSingleton2 
417156     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.16ms 
417157     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/locSet/Taclet_disjointArrayRanges.proof 
417158     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 68.11ns 
417158     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
419566     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.41s 
419566     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: disjointArrayRanges 
420439     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: disjointArrayRanges 
420448     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 5.81ms 
420449     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/locSet/Taclet_disjointArrayRangeAllFields1.proof 
420449     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 59.2ns 
420453     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
423041     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.59s 
423042     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: disjointArrayRangeAllFields1 
423827     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: disjointArrayRangeAllFields1 
423833     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.53ms 
423834     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/locSet/Taclet_disjointArrayRangeAllFields2.proof 
423834     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 52.9ns 
423835     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
426158     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.32s 
426158     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: disjointArrayRangeAllFields2 
426943     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: disjointArrayRangeAllFields2 
426949     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.88ms 
426954     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqSelfDefinition.proof 
426954     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 68.7ns 
426954     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
429170     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.22s 
429170     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqSelfDefinition 
429903     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqSelfDefinition 
429909     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.59ms 
429910     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqOutsideValue.proof 
429910     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 107.91ns 
429911     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
432134     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.22s 
432134     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqOutsideValue 
432864     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqOutsideValue 
432868     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.83ms 
432869     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_castedGetAny.proof 
432870     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 178.31ns 
432870     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
435069     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.2s 
435069     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: castedGetAny 
435842     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: castedGetAny 
435845     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.14ms 
435846     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqGetAlphaCast.proof 
435846     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 53.2ns 
435847     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
438126     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.28s 
438126     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqGetAlphaCast 
438887     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqGetAlphaCast 
438890     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 721.75ns 
438891     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqSingleton.proof 
438891     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 48.3ns 
438891     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
441159     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.27s 
441159     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqSingleton 
441881     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqSingleton 
441884     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 928.47ns 
441885     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqSingletonConcrete.proof 
441885     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 59.2ns 
441885     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
444118     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.23s 
444118     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqSingletonConcrete 
444822     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqSingletonConcrete 
444824     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 684.75ns 
444825     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqConcat.proof 
444825     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 49.8ns 
444826     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
447047     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.22s 
447047     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqConcat 
447858     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqConcat 
447868     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 7.84ms 
447872     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqSub.proof 
447872     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 70.41ns 
447872     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
450192     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.32s 
450192     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqSub 
450948     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqSub 
450951     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.26ms 
450952     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqReverse.proof 
450952     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 69.5ns 
450953     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
453150     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.2s 
453150     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqReverse 
453897     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqReverse 
453902     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.12ms 
453903     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqEmpty.proof 
453903     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 61.3ns 
453904     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
456095     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.19s 
456095     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqEmpty 
456867     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqEmpty 
456870     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 862.56ns 
456871     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqSingleton.proof 
456871     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 53ns 
456872     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
459130     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.26s 
459130     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqSingleton 
459840     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqSingleton 
459841     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 533.94ns 
459842     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqConcat.proof 
459842     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 56.2ns 
459843     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
462067     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.22s 
462067     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqConcat 
462830     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqConcat 
462832     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.08ms 
462834     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqSub.proof 
462834     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 126.31ns 
462834     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
465039     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.2s 
465039     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqSub 
465764     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqSub 
465766     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 700.95ns 
465767     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqReverse.proof 
465767     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 55.6ns 
465768     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
467997     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.23s 
467998     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqReverse 
468732     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqReverse 
468735     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 842.16ns 
468736     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_equalityToSeqGetAndSeqLenLeft.proof 
468736     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 55.6ns 
468736     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
471090     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.35s 
471090     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: equalityToSeqGetAndSeqLenLeft 
471885     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: equalityToSeqGetAndSeqLenLeft 
471887     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 812.56ns 
471888     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_equalityToSeqGetAndSeqLenRight.proof 
471888     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 54.1ns 
471888     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
474257     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.37s 
474257     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: equalityToSeqGetAndSeqLenRight 
475004     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: equalityToSeqGetAndSeqLenRight 
475008     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.02ms 
475009     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqSingletonEQ.proof 
475009     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 51.2ns 
475010     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
477373     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.36s 
477373     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqSingletonEQ 
478194     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqSingletonEQ 
478197     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 835.86ns 
478198     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqConcatEQ.proof 
478198     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 64.5ns 
478199     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
480609     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.41s 
480610     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqConcatEQ 
481428     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqConcatEQ 
481438     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 7.24ms 
481440     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqSubEQ.proof 
481440     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 220.72ns 
481441     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
483798     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.36s 
483798     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqSubEQ 
484551     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqSubEQ 
484553     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 437.83ns 
484554     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqReverseEQ.proof 
484554     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 57.7ns 
484554     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
486807     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.25s 
486807     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqReverseEQ 
487531     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqReverseEQ 
487536     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.21ms 
487537     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqEmptyEQ.proof 
487537     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 46.7ns 
487538     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
489778     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.24s 
489778     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqEmptyEQ 
490542     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqEmptyEQ 
490544     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 878.16ns 
490545     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqSingletonEQ.proof 
490545     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 57.5ns 
490546     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
492770     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.22s 
492770     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqSingletonEQ 
493510     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqSingletonEQ 
493512     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 588.14ns 
493513     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqConcatEQ.proof 
493513     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 89.81ns 
493514     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
495795     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.28s 
495795     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqConcatEQ 
496508     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqConcatEQ 
496512     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.95ms 
496516     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqSubEQ.proof 
496517     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 317.82ns 
496518     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
498757     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.24s 
498758     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqSubEQ 
499510     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqSubEQ 
499512     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 762.66ns 
499514     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqReverseEQ.proof 
499514     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 76.81ns 
499514     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
501682     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.17s 
501682     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqReverseEQ 
502419     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqReverseEQ 
502422     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 951.37ns 
502423     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqDefEQ.proof 
502423     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 48.3ns 
502423     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
504654     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.23s 
504654     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqDefEQ 
505389     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqDefEQ 
505391     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 843.86ns 
505392     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqDefEQ.proof 
505392     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 49.1ns 
505393     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
507638     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.24s 
507638     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqDefEQ 
508385     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqDefEQ 
508389     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.76ms 
508390     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqConcatWithSeqEmpty1.proof 
508390     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 59.7ns 
508390     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
510599     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.21s 
510599     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqConcatWithSeqEmpty1 
511328     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqConcatWithSeqEmpty1 
511335     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.48ms 
511336     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqConcatWithSeqEmpty2.proof 
511336     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 45.3ns 
511336     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
513563     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.23s 
513563     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqConcatWithSeqEmpty2 
514285     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqConcatWithSeqEmpty2 
514292     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 5.63ms 
514293     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqReverseOfSeqEmpty.proof 
514294     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 57.4ns 
514294     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
516500     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.21s 
516500     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqReverseOfSeqEmpty 
517224     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqReverseOfSeqEmpty 
517230     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.95ms 
517231     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_subSeqComplete.proof 
517231     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 46.8ns 
517231     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
519437     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.21s 
519437     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: subSeqComplete 
520247     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: subSeqComplete 
520253     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.32ms 
520254     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_subSeqTailR.proof 
520254     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 50.9ns 
520255     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
522500     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.25s 
522500     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: subSeqTailR 
523220     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: subSeqTailR 
523229     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 6.63ms 
523230     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_subSeqTailL.proof 
523230     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 54.4ns 
523231     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
525442     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.21s 
525442     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: subSeqTailL 
526181     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: subSeqTailL 
526190     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 7.05ms 
526191     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_subSeqTailEQR.proof 
526191     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 56.6ns 
526192     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
528518     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.33s 
528518     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: subSeqTailEQR 
529280     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: subSeqTailEQR 
529289     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 7.11ms 
529290     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_subSeqTailEQL.proof 
529291     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 64.31ns 
529291     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
531546     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.25s 
531546     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: subSeqTailEQL 
532282     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: subSeqTailEQL 
532288     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.68ms 
532289     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDef_split.proof 
532289     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 53.9ns 
532290     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
534495     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.21s 
534495     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_split 
535223     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDef_split 
535240     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 14.81ms 
535241     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDef_induction_upper.proof 
535242     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 85.81ns 
535242     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
537475     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.23s 
537475     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_induction_upper 
538236     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDef_induction_upper 
538255     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 16.3ms 
538257     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDef_induction_upper_concrete.proof 
538257     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 68.61ns 
538257     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
540569     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.31s 
540569     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_induction_upper_concrete 
541385     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDef_induction_upper_concrete 
541402     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 13.92ms 
541404     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDef_induction_lower.proof 
541404     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 73.5ns 
541405     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
543800     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.4s 
543801     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_induction_lower 
544565     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDef_induction_lower 
544582     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 13.34ms 
544583     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDef_induction_lower_concrete.proof 
544583     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 73.51ns 
544584     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
546815     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.23s 
546815     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_induction_lower_concrete 
547628     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDef_induction_lower_concrete 
547648     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 16.86ms 
547650     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDef_split_in_three.proof 
547650     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 60.1ns 
547651     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
549919     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.27s 
549919     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_split_in_three 
550666     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDef_split_in_three 
550712     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 38.51ms 
550714     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDef_empty.proof 
550714     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 71.31ns 
550714     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
552998     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.28s 
552998     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_empty 
553747     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDef_empty 
553751     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.24ms 
553752     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDef_one_summand.proof 
553752     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 45.9ns 
553753     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
556015     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.26s 
556015     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_one_summand 
556789     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDef_one_summand 
556794     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.25ms 
556795     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDef_lower_equals_upper.proof 
556795     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 64.8ns 
556796     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
559014     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.22s 
559015     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_lower_equals_upper 
559752     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDef_lower_equals_upper 
559755     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.54ms 
559756     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDefOfSeq.proof 
559756     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 56ns 
559757     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
561977     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.22s 
561977     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDefOfSeq 
562719     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDefOfSeq 
562731     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 9.49ms 
562732     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqSelfDefinitionEQ2.proof 
562732     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 58.91ns 
562733     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
565101     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.37s 
565101     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqSelfDefinitionEQ2 
565858     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqSelfDefinitionEQ2 
565863     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.67ms 
565864     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_indexOfSeqSingleton.proof 
565865     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 68.5ns 
565865     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
568261     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.4s 
568261     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: indexOfSeqSingleton 
569029     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: indexOfSeqSingleton 
569032     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.27ms 
569033     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_indexOfSeqConcatFirst.proof 
569033     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 64.5ns 
569034     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
571391     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.36s 
571391     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: indexOfSeqConcatFirst 
572199     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: indexOfSeqConcatFirst 
572209     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 8.33ms 
572211     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_indexOfSeqConcatSecond.proof 
572211     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 62ns 
572211     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
574798     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.59s 
574798     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: indexOfSeqConcatSecond 
575642     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: indexOfSeqConcatSecond 
575654     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 9.3ms 
575655     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_indexOfSeqSub.proof 
575655     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 69.11ns 
575656     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
578169     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.51s 
578169     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: indexOfSeqSub 
578984     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: indexOfSeqSub 
578999     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 11.75ms 
579000     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfArray2seq.proof 
579000     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 72.41ns 
579001     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
581444     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.44s 
581444     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfArray2seq 
582276     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfArray2seq 
582279     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 981.47ns 
582280     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getAnyOfArray2seq.proof 
582280     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 56.6ns 
582281     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
584788     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.51s 
584788     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getAnyOfArray2seq 
585600     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getAnyOfArray2seq 
585603     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.57ms 
585604     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfArray2seq.proof 
585604     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 56.5ns 
585605     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
588055     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.45s 
588055     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfArray2seq 
588907     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfArray2seq 
588913     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.02ms 
588914     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_getAnyOfNPermInv.proof 
588914     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 84.91ns 
588915     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
591391     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.48s 
591392     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getAnyOfNPermInv 
592214     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getAnyOfNPermInv 
592218     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.7ms 
592219     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqNPermRange.proof 
592219     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 61.3ns 
592220     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
594677     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.46s 
594677     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqNPermRange 
595444     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqNPermRange 
595483     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 33.18ms 
595484     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermTrans.proof 
595484     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 62.2ns 
595485     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
597745     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.26s 
597746     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermTrans 
598518     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermTrans 
598534     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 12.37ms 
598535     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermRefl.proof 
598535     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 67.7ns 
598535     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
600745     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.21s 
600746     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermRefl 
601472     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermRefl 
601482     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 7.27ms 
601483     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermSplit.proof 
601483     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 57.6ns 
601483     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
603713     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.23s 
603713     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermSplit 
604501     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermSplit 
604503     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 193.91ns 
604505     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqNPermRight.proof 
604505     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 204.32ns 
604507     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
606701     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.19s 
606701     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqNPermRight 
607426     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqNPermRight 
607498     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 61.28ms 
607499     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermFromSwap.proof 
607499     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 60.2ns 
607500     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
609741     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.24s 
609741     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermFromSwap 
610478     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermFromSwap 
610507     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 24.83ms 
610508     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermTransAlt0.proof 
610508     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 50.5ns 
610509     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
612699     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.19s 
612699     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermTransAlt0 
613426     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermTransAlt0 
613428     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 250.92ns 
613430     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermTransAlt1.proof 
613430     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 108.41ns 
613430     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
615666     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.24s 
615666     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermTransAlt1 
616370     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermTransAlt1 
616372     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 166.71ns 
616374     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermTransAlt2.proof 
616374     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 124.01ns 
616374     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
618570     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.2s 
618570     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermTransAlt2 
619341     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermTransAlt2 
619343     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 224.02ns 
619344     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermTransAlt3.proof 
619344     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 55.8ns 
619345     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
621532     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.19s 
621532     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermTransAlt3 
622267     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermTransAlt3 
622269     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 383.33ns 
622271     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermForall.proof 
622271     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 56.2ns 
622271     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
624596     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.33s 
624596     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermForall 
625448     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermForall 
625551     INFO  Test worker     d.u.i.k.s.SMTFocusResults Analyzing unsat core: (L_1 L_3 L_4) 
625563     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 112.55ms 
625566     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermExists.proof 
625566     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 224.82ns 
625567     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
628044     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.48s 
628045     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermExists 
628850     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermExists 
628926     INFO  Test worker     d.u.i.k.s.SMTFocusResults Analyzing unsat core: (L_1 L_3 L_5 L_6 L_7) 
628927     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 74.8ms 
628929     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm2/Taclet_schiffl_lemma_2.proof 
628929     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 83.21ns 
628930     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
631334     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.4s 
631334     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: schiffl_lemma_2 
632129     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: schiffl_lemma_2 
632131     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.6ns 
632162     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [1] goal: 0, source line: 49, command: 'macro split-prop' 
632191     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [2] goal: 3, source line: 50, command: 'rule allRight' 
632202     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [3] goal: 4, source line: 51, command: 'rule allRight' 
632205     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [4] goal: 5, source line: 52, command: 'macro split-prop' 
632213     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [5] goal: 11, source line: 53, command: 'rule 'seqPermDefLeft'' 
632214     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [6] goal: 12, source line: 54, command: 'rule 'andLeft'' 
632216     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [7] goal: 13, source line: 55, command: 'rule 'exLeft'' 
632217     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [8] goal: 14, source line: 56, command: 'macro split-prop' 
632220     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [9] goal: 16, source line: 57, command: 'rule  seqNPermRange' 
632221     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' 
632223     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [11] goal: 18, source line: 60, command: 'rule impLeft' 
632224     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [12] goal: 19, source line: 61, command: 'tryclose branch' 
632440     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [13] goal: 20, source line: 62, command: 'rule andLeft' 
632442     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [14] goal: 97, source line: 63, command: 'rule andLeft' 
632445     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' 
632445     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [16] goal: 99, source line: 66, command: 'rule impLeft' 
632447     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [17] goal: 100, source line: 67, command: 'tryclose branch' 
632587     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [18] goal: 101, source line: 68, command: 'rule andLeft' 
632588     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [19] goal: 188, source line: 69, command: 'rule andLeft' 
632591     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [20] goal: 189, source line: 70, command: 'rule seqNPermDefLeft' 
632593     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' 
632594     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [22] goal: 191, source line: 73, command: 'rule impLeft' 
632596     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [23] goal: 192, source line: 74, command: 'tryclose branch' 
632809     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [24] goal: 193, source line: 75, command: 'rule exLeft' 
632811     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [25] goal: 310, source line: 76, command: 'rule andLeft' 
632812     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [26] goal: 311, source line: 77, command: 'rule andLeft' 
632813     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' 
632813     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [28] goal: 313, source line: 80, command: 'rule impLeft' 
632816     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [29] goal: 314, source line: 81, command: 'tryclose branch' 
632982     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [30] goal: 315, source line: 82, command: 'rule exLeft' 
632983     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [31] goal: 420, source line: 83, command: 'rule andLeft' 
632984     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [32] goal: 421, source line: 84, command: 'rule andLeft' 
632985     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' 
632986     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [34] goal: 423, source line: 87, command: 'rule impLeft' 
632987     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [35] goal: 424, source line: 88, command: 'tryclose branch' 
632996     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [36] goal: 425, source line: 89, command: 'rule andLeft' 
632997     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [37] goal: 434, source line: 90, command: 'rule andLeft' 
633000     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' 
633000     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' 
633002     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [40] goal: 437, source line: 94, command: 'rule impLeft' 
633003     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [41] goal: 438, source line: 95, command: 'tryclose branch' 
633013     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [42] goal: 439, source line: 96, command: 'rule andLeft' 
633014     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [43] goal: 448, source line: 97, command: 'rule andLeft' 
633017     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' 
633018     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [45] goal: 450, source line: 99, command: 'instantiate var=iv  with='v_x_0'' 
633019     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [46] goal: 451, source line: 101, command: 'rule impLeft' 
633020     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [47] goal: 452, source line: 102, command: 'tryclose branch' 
633222     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [48] goal: 453, source line: 103, command: 'instantiate var=iv  with='v_y_0'' 
633223     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [49] goal: 562, source line: 105, command: 'rule impLeft' 
633224     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [50] goal: 563, source line: 106, command: 'tryclose branch' 
633366     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [51] goal: 564, source line: 107, command: 'cut 'v_x_0 = v_y_0'' 
633367     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)'' 
633368     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [53] goal: 676, source line: 111, command: 'rule andRight' 
633370     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [54] goal: 677, source line: 113, command: 'rule andRight' 
633371     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [55] goal: 679, source line: 114, command: 'rule andRight' 
633372     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [56] goal: 681, source line: 115, command: 'rule andRight' 
633374     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [57] goal: 683, source line: 116, command: 'rule lenOfSwap' 
633375     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [58] goal: 685, source line: 117, command: 'tryclose branch' 
633379     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [59] goal: 684, source line: 118, command: 'rule seqNPermSwapNPerm' 
633380     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' 
633381     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [61] goal: 688, source line: 121, command: 'instantiate hide var='jv' with='jv_0'' 
633382     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [62] goal: 689, source line: 122, command: 'rule impLeft' 
633382     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [63] goal: 690, source line: 123, command: 'tryclose branch' 
633500     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [64] goal: 691, source line: 124, command: 'tryclose branch' 
633504     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [65] goal: 682, source line: 125, command: 'rule allRight' 
633505     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [66] goal: 796, source line: 127, command: 'rule impRight' 
633506     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [67] goal: 797, source line: 128, command: 'rule andLeft' 
633507     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [68] goal: 798, source line: 129, command: 'instantiate var=iv with='v_iv_0'' 
633508     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [69] goal: 799, source line: 130, command: 'rule impLeft' 
633512     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [70] goal: 800, source line: 131, command: 'tryclose branch' 
633673     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [71] goal: 801, source line: 132, command: 'rule getOfSwap' 
633674     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [72] goal: 912, source line: 133, command: 'rule ifthenelse_negated' 
633676     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [73] goal: 913, source line: 134, command: 'rule ifthenelse_split occ=0' 
633677     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [74] goal: 914, source line: 135, command: 'rule andLeft' 
633678     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [75] goal: 916, source line: 136, command: 'rule andLeft' 
633679     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [76] goal: 917, source line: 137, command: 'rule andLeft' 
633681     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [77] goal: 918, source line: 138, command: 'rule ifthenelse_split occ=0' 
633681     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [78] goal: 919, source line: 139, command: 'tryclose branch' 
633809     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [79] goal: 920, source line: 140, command: 'rule ifthenelse_split occ=0' 
633810     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [80] goal: 1011, source line: 141, command: 'tryclose branch' 
633926     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [81] goal: 1012, source line: 142, command: 'tryclose branch' 
633931     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [82] goal: 915, source line: 143, command: 'tryclose branch' 
633938     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [83] goal: 680, source line: 144, command: 'rule getOfSwap' 
633938     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [84] goal: 1099, source line: 146, command: 'rule ifthenelse_negated' 
633942     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [85] goal: 1100, source line: 147, command: 'rule ifthenelse_split occ=0' 
633943     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [86] goal: 1101, source line: 148, command: 'rule andLeft' 
633943     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [87] goal: 1103, source line: 149, command: 'rule andLeft' 
633944     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [88] goal: 1104, source line: 150, command: 'rule andLeft' 
633945     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [89] goal: 1105, source line: 151, command: 'rule ifthenelse_split occ=0' 
633946     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [90] goal: 1106, source line: 152, command: 'tryclose branch' 
633956     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [91] goal: 1107, source line: 153, command: 'tryclose branch' 
633962     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [92] goal: 1102, source line: 154, command: 'tryclose branch' 
634104     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [93] goal: 678, source line: 155, command: 'rule getOfSwap' 
634105     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [94] goal: 1225, source line: 157, command: 'rule ifthenelse_negated' 
634107     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [95] goal: 1226, source line: 158, command: 'rule ifthenelse_split occ=0' 
634108     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [96] goal: 1227, source line: 159, command: 'rule andLeft' 
634109     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [97] goal: 1229, source line: 160, command: 'rule andLeft' 
634109     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [98] goal: 1230, source line: 161, command: 'rule andLeft' 
634110     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [99] goal: 1231, source line: 162, command: 'rule ifthenelse_split occ=0' 
634110     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [100] goal: 1232, source line: 163, command: 'tryclose branch' 
634175     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [101] goal: 1233, source line: 164, command: 'tryclose branch' 
634182     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [102] goal: 1228, source line: 165, command: 'tryclose branch' 
634289     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]'' 
634290     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [104] goal: 1397, source line: 169, command: 'rule seqNPermInjective' 
634292     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'' 
634294     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'' 
634295     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [107] goal: 1401, source line: 172, command: 'rule impLeft' 
634296     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [108] goal: 1402, source line: 173, command: 'tryclose branch' 
634442     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [109] goal: 1403, source line: 174, command: 'tryclose branch' 
634447     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'' 
634449     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)'' 
634450     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [112] goal: 1536, source line: 179, command: 'rule andRight' 
634452     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [113] goal: 1537, source line: 181, command: 'rule andRight' 
634452     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [114] goal: 1539, source line: 182, command: 'rule andRight' 
634453     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [115] goal: 1541, source line: 183, command: 'rule andRight' 
634454     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [116] goal: 1543, source line: 184, command: 'tryclose branch' 
634464     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [117] goal: 1544, source line: 185, command: 'rule seqNPermSwapNPerm' 
634469     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'' 
634470     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [119] goal: 1559, source line: 188, command: 'instantiate hide var=jv with='jv_1'' 
634472     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [120] goal: 1560, source line: 189, command: 'tryclose branch' 
634562     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [121] goal: 1542, source line: 190, command: 'rule allRight' 
634562     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [122] goal: 1667, source line: 192, command: 'rule impRight' 
634564     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [123] goal: 1668, source line: 193, command: 'rule andLeft' 
634564     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [124] goal: 1669, source line: 194, command: 'instantiate var=iv with='v_iv_0'' 
634565     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [125] goal: 1670, source line: 195, command: 'rule impLeft' 
634566     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [126] goal: 1671, source line: 196, command: 'tryclose branch' 
634669     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [127] goal: 1672, source line: 197, command: 'rule getOfSwap' 
634670     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [128] goal: 1786, source line: 198, command: 'rule ifthenelse_negated' 
634672     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [129] goal: 1787, source line: 199, command: 'rule ifthenelse_split occ=0' 
634673     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [130] goal: 1788, source line: 200, command: 'rule andLeft' 
634674     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [131] goal: 1790, source line: 201, command: 'rule andLeft' 
634674     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [132] goal: 1791, source line: 202, command: 'rule andLeft' 
634675     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [133] goal: 1792, source line: 203, command: 'rule ifthenelse_split occ=0' 
634676     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [134] goal: 1793, source line: 204, command: 'tryclose branch' 
634763     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [135] goal: 1794, source line: 205, command: 'rule ifthenelse_split occ=0' 
634764     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [136] goal: 1885, source line: 206, command: 'tryclose branch' 
634846     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [137] goal: 1886, source line: 207, command: 'instantiate var=iv with='v_y_0'' 
634847     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [138] goal: 1968, source line: 208, command: 'rule impLeft' 
634847     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [139] goal: 1969, source line: 209, command: 'tryclose branch' 
634852     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [140] goal: 1970, source line: 210, command: 'tryclose branch' 
634856     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [141] goal: 1789, source line: 211, command: 'tryclose branch' 
634861     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [142] goal: 1540, source line: 212, command: 'tryclose branch' 
635008     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [143] goal: 1538, source line: 213, command: 'rule getOfSwap' 
635009     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [144] goal: 2097, source line: 215, command: 'rule ifthenelse_negated' 
635010     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [145] goal: 2098, source line: 216, command: 'rule ifthenelse_split occ=0' 
635011     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [146] goal: 2099, source line: 217, command: 'tryclose branch' 
635022     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [147] goal: 2100, source line: 218, command: 'tryclose branch' 
635122     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [148] goal: 1535, source line: 219, command: 'tryclose branch' 
638708     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'' 
638709     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)'' 
638714     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [151] goal: 4268, source line: 226, command: 'rule andRight' 
638715     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [152] goal: 4269, source line: 228, command: 'rule andRight' 
638716     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [153] goal: 4271, source line: 229, command: 'rule andRight' 
638717     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [154] goal: 4273, source line: 230, command: 'rule andRight' 
638717     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [155] goal: 4275, source line: 231, command: 'tryclose branch' 
638726     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [156] goal: 4276, source line: 232, command: 'rule seqNPermSwapNPerm' 
638727     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'' 
638728     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [158] goal: 4288, source line: 235, command: 'instantiate hide var=jv with='jv_0'' 
638729     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [159] goal: 4289, source line: 236, command: 'rule impLeft' 
638730     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [160] goal: 4290, source line: 237, command: 'tryclose branch' 
638831     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [161] goal: 4291, source line: 238, command: 'tryclose branch' 
638835     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [162] goal: 4274, source line: 239, command: 'rule allRight' 
638836     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [163] goal: 4400, source line: 241, command: 'rule impRight' 
638837     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [164] goal: 4401, source line: 242, command: 'rule andLeft' 
638838     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [165] goal: 4402, source line: 243, command: 'instantiate var=iv with='v_iv_0'' 
638838     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [166] goal: 4403, source line: 244, command: 'rule impLeft' 
638839     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [167] goal: 4404, source line: 245, command: 'tryclose branch' 
638933     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [168] goal: 4405, source line: 246, command: 'rule getOfSwap' 
638934     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [169] goal: 4521, source line: 247, command: 'rule ifthenelse_negated' 
638935     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [170] goal: 4522, source line: 248, command: 'rule ifthenelse_split occ=0' 
638936     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [171] goal: 4523, source line: 249, command: 'rule andLeft' 
638937     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [172] goal: 4525, source line: 250, command: 'rule andLeft' 
638937     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [173] goal: 4526, source line: 251, command: 'rule andLeft' 
638938     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [174] goal: 4527, source line: 252, command: 'rule ifthenelse_split occ=0' 
638939     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [175] goal: 4528, source line: 253, command: 'tryclose branch' 
639017     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [176] goal: 4529, source line: 254, command: 'rule ifthenelse_split occ=0' 
639018     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [177] goal: 4622, source line: 255, command: 'tryclose branch' 
639090     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [178] goal: 4623, source line: 256, command: 'tryclose branch' 
639094     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [179] goal: 4524, source line: 257, command: 'tryclose branch' 
639098     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [180] goal: 4272, source line: 258, command: 'rule getOfSwap' 
639099     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [181] goal: 4713, source line: 260, command: 'rule ifthenelse_negated' 
639100     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [182] goal: 4714, source line: 261, command: 'rule ifthenelse_split occ=0' 
639101     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [183] goal: 4715, source line: 262, command: 'tryclose branch' 
639111     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [184] goal: 4716, source line: 263, command: 'tryclose branch' 
639188     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [185] goal: 4270, source line: 264, command: 'rule getOfSwap' 
639189     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [186] goal: 4839, source line: 266, command: 'rule ifthenelse_negated' 
639189     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [187] goal: 4840, source line: 267, command: 'rule ifthenelse_split occ=0' 
639190     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [188] goal: 4841, source line: 268, command: 'tryclose branch' 
639262     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [189] goal: 4842, source line: 269, command: 'tryclose branch' 
639272     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'' 
639273     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)'' 
639274     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [192] goal: 4950, source line: 275, command: 'rule andRight' 
639275     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [193] goal: 4951, source line: 277, command: 'rule andRight' 
639276     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [194] goal: 4953, source line: 278, command: 'rule andRight' 
639276     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [195] goal: 4955, source line: 279, command: 'rule andRight' 
639277     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [196] goal: 4957, source line: 280, command: 'tryclose branch' 
639288     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [197] goal: 4958, source line: 281, command: 'rule seqNPermSwapNPerm' 
639288     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [198] goal: 4977, source line: 283, command: 'instantiate hide var=iv with='jv_0'' 
639289     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'' 
639290     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [200] goal: 4979, source line: 285, command: 'rule impLeft' 
639291     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [201] goal: 4980, source line: 286, command: 'tryclose branch' 
639383     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))'' 
639384     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [203] goal: 5093, source line: 288, command: 'instantiate hide var=iv with='jv_0'' 
639385     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'' 
639386     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [205] goal: 5095, source line: 290, command: 'rule impLeft' 
639387     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [206] goal: 5096, source line: 291, command: 'tryclose branch' 
639478     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [207] goal: 5097, source line: 292, command: 'tryclose branch' 
639483     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [208] goal: 4956, source line: 293, command: 'rule allRight' 
639483     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [209] goal: 5212, source line: 295, command: 'rule impRight' 
639484     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [210] goal: 5213, source line: 296, command: 'rule andLeft' 
639485     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [211] goal: 5214, source line: 297, command: 'instantiate var=iv with='v_iv_0'' 
639485     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [212] goal: 5215, source line: 300, command: 'rule impLeft' 
639486     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [213] goal: 5216, source line: 301, command: 'tryclose branch' 
639588     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [214] goal: 5217, source line: 302, command: 'rule getOfSwap' 
639589     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [215] goal: 5337, source line: 304, command: 'rule ifthenelse_negated' 
639590     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [216] goal: 5338, source line: 305, command: 'rule ifthenelse_split occ=0' 
639591     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [217] goal: 5339, source line: 306, command: 'rule andLeft' 
639592     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [218] goal: 5341, source line: 307, command: 'rule andLeft' 
639592     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [219] goal: 5342, source line: 308, command: 'rule andLeft' 
639593     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [220] goal: 5343, source line: 309, command: 'rule ifthenelse_split occ=0' 
639593     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [221] goal: 5344, source line: 310, command: 'rule getOfSwap' 
639594     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [222] goal: 5346, source line: 311, command: 'rule ifthenelse_negated' 
639595     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [223] goal: 5347, source line: 312, command: 'rule ifthenelse_split occ=0' 
639596     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [224] goal: 5348, source line: 313, command: 'rule andLeft' 
639596     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [225] goal: 5350, source line: 314, command: 'rule andLeft' 
639597     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [226] goal: 5351, source line: 315, command: 'rule andLeft' 
639597     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [227] goal: 5352, source line: 316, command: 'rule ifthenelse_split occ=0' 
639598     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [228] goal: 5353, source line: 317, command: 'tryclose branch' 
639690     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [229] goal: 5354, source line: 318, command: 'rule ifthenelse_split occ=0' 
639691     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [230] goal: 5463, source line: 319, command: 'tryclose branch' 
639697     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [231] goal: 5464, source line: 320, command: 'tryclose branch' 
639773     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [232] goal: 5349, source line: 321, command: 'tryclose branch' 
639849     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [233] goal: 5345, source line: 322, command: 'rule ifthenelse_split' 
639850     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [234] goal: 5660, source line: 324, command: 'rule getOfSwap' 
639851     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [235] goal: 5662, source line: 325, command: 'rule ifthenelse_negated' 
639851     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [236] goal: 5663, source line: 326, command: 'rule ifthenelse_split occ=0' 
639852     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [237] goal: 5664, source line: 327, command: 'rule andLeft' 
639853     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [238] goal: 5666, source line: 328, command: 'rule andLeft' 
639853     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [239] goal: 5667, source line: 329, command: 'rule andLeft' 
639853     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [240] goal: 5668, source line: 330, command: 'rule ifthenelse_split occ=0' 
639854     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [241] goal: 5669, source line: 331, command: 'tryclose branch' 
639937     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [242] goal: 5670, source line: 332, command: 'tryclose branch' 
639943     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [243] goal: 5665, source line: 333, command: 'tryclose branch' 
640026     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [244] goal: 5661, source line: 334, command: 'rule getOfSwap' 
640027     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [245] goal: 5887, source line: 336, command: 'rule ifthenelse_negated' 
640028     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [246] goal: 5888, source line: 337, command: 'rule ifthenelse_split occ=0' 
640028     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [247] goal: 5889, source line: 338, command: 'rule andLeft' 
640029     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [248] goal: 5891, source line: 339, command: 'rule andLeft' 
640029     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [249] goal: 5892, source line: 340, command: 'rule andLeft' 
640030     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [250] goal: 5893, source line: 341, command: 'rule ifthenelse_split occ=0' 
640030     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [251] goal: 5894, source line: 342, command: 'tryclose branch' 
640035     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [252] goal: 5895, source line: 343, command: 'rule ifthenelse_split occ=0' 
640036     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [253] goal: 5897, source line: 344, command: 'tryclose branch' 
640111     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [254] goal: 5898, source line: 345, command: 'tryclose branch' 
640117     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [255] goal: 5890, source line: 346, command: 'tryclose branch' 
640122     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [256] goal: 5340, source line: 347, command: 'tryclose branch' 
640271     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [257] goal: 4954, source line: 348, command: 'rule getOfSwap' 
640272     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [258] goal: 6115, source line: 350, command: 'rule ifthenelse_negated' 
640273     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [259] goal: 6116, source line: 351, command: 'rule ifthenelse_split occ=0' 
640274     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [260] goal: 6117, source line: 352, command: 'rule andLeft' 
640274     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [261] goal: 6119, source line: 353, command: 'rule andLeft' 
640274     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [262] goal: 6120, source line: 354, command: 'rule andLeft' 
640275     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [263] goal: 6121, source line: 355, command: 'rule ifthenelse_split occ=0' 
640275     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [264] goal: 6122, source line: 356, command: 'tryclose branch' 
640327     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [265] goal: 6123, source line: 357, command: 'rule ifthenelse_split occ=0' 
640328     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [266] goal: 6193, source line: 358, command: 'rule getOfSwap' 
640328     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [267] goal: 6195, source line: 359, command: 'rule ifthenelse_negated' 
640329     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [268] goal: 6196, source line: 360, command: 'rule ifthenelse_split occ=0' 
640329     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [269] goal: 6197, source line: 361, command: 'tryclose branch' 
640335     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [270] goal: 6198, source line: 362, command: 'tryclose branch' 
640340     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [271] goal: 6194, source line: 363, command: 'tryclose branch' 
640453     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [272] goal: 6118, source line: 364, command: 'tryclose branch' 
640538     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [273] goal: 4952, source line: 365, command: 'rule getOfSwap' 
640538     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [274] goal: 6456, source line: 367, command: 'rule ifthenelse_negated' 
640539     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [275] goal: 6457, source line: 368, command: 'rule ifthenelse_split occ=0' 
640540     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [276] goal: 6458, source line: 369, command: 'tryclose branch' 
640702     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [277] goal: 6459, source line: 370, command: 'tryclose branch' 
640788     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'' 
640788     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [279] goal: 6735, source line: 375, command: 'tryclose branch' 
643695     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [280] goal: 6735, source line: 378, command: 'rule seqNPermSwapNPerm' 
643698     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [281] goal: 8783, source line: 380, command: 'instantiate hide var=iv with='jv_1'' 
643699     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'' 
643700     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [283] goal: 8785, source line: 382, command: 'rule impLeft' 
643701     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [284] goal: 8786, source line: 383, command: 'tryclose branch' 
643810     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))'' 
643811     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [286] goal: 8909, source line: 385, command: 'instantiate hide var=iv with='jv_1'' 
643812     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'' 
643813     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [288] goal: 8911, source line: 387, command: 'rule impLeft' 
643813     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [289] goal: 8912, source line: 388, command: 'tryclose branch' 
643969     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [290] goal: 8913, source line: 389, command: 'tryclose branch' 
646983     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [291] goal: 6736, source line: 390, command: 'tryclose branch' 
650385     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [292] goal: 6736, source line: 397, command: 'rule seqNPermSwapNPerm formula='seqNPerm(s_0)'' 
650389     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'' 
650390     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [294] goal: 12634, source line: 400, command: 'instantiate hide var=jv with='jv_0'' 
650391     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [295] goal: 12635, source line: 401, command: 'rule impLeft' 
650392     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [296] goal: 12636, source line: 402, command: 'tryclose branch' 
650508     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))'' 
650508     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'' 
650509     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [299] goal: 12758, source line: 405, command: 'instantiate hide var=jv with='jv_1'' 
650511     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)' ...' 
650511     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [301] goal: 12760, source line: 407, command: 'tryclose branch' 
651675     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm2/Taclet_schiffl_thm_1.proof 
651675     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 104.61ns 
651676     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
654355     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.68s 
654355     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: schiffl_thm_1 
655265     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: schiffl_thm_1 
655266     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 7ns 
655267     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [1] goal: 0, source line: 50, command: 'macro split-prop' 
655273     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)'' 
655283     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [3] goal: 11, source line: 52, command: 'instantiate hide var=x with='f_x'' 
655285     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [4] goal: 12, source line: 53, command: 'instantiate hide var=y with='f_y'' 
655287     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [5] goal: 13, source line: 54, command: 'rule impLeft' 
655289     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [6] goal: 14, source line: 55, command: 'tryclose branch' 
655293     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [7] goal: 15, source line: 56, command: 'rule exLeft' 
655294     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [8] goal: 23, source line: 57, command: 'macro split-prop' 
655298     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [9] goal: 27, source line: 58, command: 'rule seqPermDef occ=1' 
655298     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [10] goal: 28, source line: 59, command: 'rule andRight' 
655300     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [11] goal: 29, source line: 60, command: 'tryclose branch' 
655310     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [12] goal: 30, source line: 61, command: 'instantiate hide var=s with='r_0'' 
655310     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [13] goal: 46, source line: 62, command: 'rule andRight' 
655312     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [14] goal: 47, source line: 63, command: 'tryclose branch' 
655364     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [15] goal: 48, source line: 64, command: 'rule allRight' 
655365     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [16] goal: 119, source line: 65, command: 'rule impRight' 
655365     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [17] goal: 120, source line: 66, command: 'instantiate hide var=iv with='iv_0'' 
655366     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [18] goal: 121, source line: 67, command: 'rule impLeft' 
655366     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [19] goal: 122, source line: 68, command: 'tryclose branch' 
655436     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [20] goal: 123, source line: 69, command: 'rule andLeft' 
655437     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [21] goal: 203, source line: 70, command: 'rule seqNPermRange' 
655438     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [22] goal: 204, source line: 71, command: 'instantiate hide var=iv with='iv_0'' 
655438     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [23] goal: 205, source line: 72, command: 'rule impLeft' 
655439     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [24] goal: 206, source line: 73, command: 'tryclose branch' 
655443     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [25] goal: 207, source line: 74, command: 'rule andLeft' 
655444     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [26] goal: 215, source line: 75, command: 'rule andLeft' 
655444     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [27] goal: 216, source line: 76, command: 'rule seqNPermRange' 
655445     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [28] goal: 217, source line: 77, command: 'instantiate hide var=iv with='f_x'' 
655446     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [29] goal: 218, source line: 78, command: 'rule impLeft' 
655446     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [30] goal: 219, source line: 79, command: 'tryclose branch' 
655532     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [31] goal: 220, source line: 80, command: 'rule andLeft' 
655532     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [32] goal: 311, source line: 81, command: 'rule andLeft' 
655533     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [33] goal: 312, source line: 82, command: 'rule seqNPermRange' 
655533     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [34] goal: 313, source line: 83, command: 'instantiate hide var=iv with='f_y'' 
655534     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [35] goal: 314, source line: 84, command: 'rule impLeft' 
655535     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [36] goal: 315, source line: 85, command: 'tryclose branch' 
655624     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [37] goal: 316, source line: 86, command: 'rule andLeft' 
655625     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [38] goal: 410, source line: 87, command: 'rule andLeft' 
655626     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [39] goal: 411, source line: 88, command: 'rule getOfSeqDef occ=0' 
655626     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [40] goal: 412, source line: 89, command: 'rule getOfSeqDef' 
655627     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [41] goal: 413, source line: 90, command: 'rule ifthenelse_split occ=0' 
655628     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [42] goal: 414, source line: 91, command: 'rule andLeft occ=0' 
655628     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [43] goal: 416, source line: 92, command: 'rule sub_zero_2 occ=0' 
655629     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [44] goal: 417, source line: 93, command: 'rule ifthenelse_split occ=2' 
655629     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [45] goal: 418, source line: 94, command: 'rule andLeft' 
655630     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [46] goal: 420, source line: 95, command: 'rule sub_zero_2 occ=0' 
655630     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [47] goal: 421, source line: 96, command: 'rule add_zero_right occ=0' 
655631     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [48] goal: 422, source line: 97, command: 'rule add_zero_right occ=0' 
655631     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [49] goal: 423, source line: 98, command: 'rule add_zero_right occ=0' 
655632     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [50] goal: 424, source line: 99, command: 'rule add_zero_right occ=0' 
655633     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [51] goal: 425, source line: 100, command: 'rule add_zero_right occ=0' 
655633     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [52] goal: 426, source line: 101, command: 'rule add_zero_right occ=0' 
655634     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [53] goal: 427, source line: 102, command: 'rule ifthenelse_split occ=0' 
655634     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [54] goal: 428, source line: 103, command: 'rule ifthenelse_split occ=0' 
655635     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [55] goal: 430, source line: 104, command: 'tryclose branch' 
655638     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [56] goal: 431, source line: 105, command: 'tryclose branch' 
655679     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [57] goal: 429, source line: 106, command: 'rule ifthenelse_split occ=0' 
655680     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [58] goal: 473, source line: 107, command: 'tryclose branch' 
655742     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [59] goal: 474, source line: 108, command: 'rule ifthenelse_split occ=0' 
655743     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [60] goal: 541, source line: 109, command: 'rule seqNPermInjective' 
655744     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [61] goal: 543, source line: 110, command: 'instantiate hide var=iv with='iv_0'' 
655745     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [62] goal: 544, source line: 111, command: 'instantiate hide var=jv with='f_y'' 
655746     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [63] goal: 545, source line: 112, command: 'rule impLeft' 
655747     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [64] goal: 546, source line: 113, command: 'tryclose branch' 
655800     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [65] goal: 547, source line: 114, command: 'tryclose branch' 
655803     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [66] goal: 542, source line: 115, command: 'rule ifthenelse_split occ=0' 
655804     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [67] goal: 606, source line: 116, command: 'rule seqNPermInjective' 
655805     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [68] goal: 608, source line: 117, command: 'instantiate hide var=iv with='iv_0'' 
655806     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [69] goal: 609, source line: 118, command: 'instantiate hide var=jv with='f_x'' 
655807     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [70] goal: 610, source line: 119, command: 'rule impLeft' 
655808     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [71] goal: 611, source line: 120, command: 'tryclose branch' 
655856     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [72] goal: 612, source line: 121, command: 'tryclose branch' 
655858     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [73] goal: 607, source line: 122, command: 'tryclose branch' 
655862     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [74] goal: 419, source line: 123, command: 'tryclose branch' 
655917     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [75] goal: 415, source line: 124, command: 'tryclose branch' 
655974     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_eqSameSeq.proof 
655974     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 232.82ns 
655975     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
658560     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.59s 
658560     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: eqSameSeq 
659371     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: eqSameSeq 
659387     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 12.16ms