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

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

tests
0

failures
0

ignored
10m50.78s

duration
100%

successful

Tests

Test Method name Duration Result
powPositive data()[100] 3.151s passed
powPositiveConcrete data()[101] 3.164s passed
powGeq1Concrete data()[102] 3.144s passed
pow2InIntLower data()[103] 3.149s passed
pow2InIntUpper data()[104] 3.172s passed
logSelfConcrete data()[105] 3.173s passed
log1Concrete data()[106] 3.168s passed
logProduct data()[107] 3.168s passed
logTimesBaseConcrete data()[108] 3.173s passed
logProdIdentity data()[109] 3.184s passed
moduloByteIsInByte data()[10] 3.245s passed
logProdIdentityConcrete data()[110] 3.197s passed
logPowIdentity data()[111] 3.216s passed
logPowIdentityConcrete data()[112] 3.150s passed
logPositive data()[113] 3.171s passed
logPositiveConcrete data()[114] 3.151s passed
logMono data()[115] 3.178s passed
logMonoConcrete data()[116] 3.149s passed
powLogLess data()[117] 3.178s passed
powLogMore2 data()[118] 3.190s passed
logLessThanPow data()[119] 3.190s passed
moduloCharIsInChar data()[11] 3.200s passed
logLessThanPowConcrete data()[120] 3.169s passed
logSqueeze data()[121] 3.156s passed
ifthenelse_equals data()[122] 3.197s passed
ifthenelse_equals_1 data()[123] 3.272s passed
ifthenelse_equals_2 data()[124] 3.268s passed
disjointWithSingleton1 data()[125] 3.189s passed
disjointWithSingleton2 data()[126] 3.157s passed
disjointArrayRanges data()[127] 3.178s passed
disjointArrayRangeAllFields1 data()[128] 3.148s passed
disjointArrayRangeAllFields2 data()[129] 3.182s passed
div_unique1 data()[12] 3.274s passed
seqSelfDefinition data()[130] 3.179s passed
seqOutsideValue data()[131] 3.157s passed
castedGetAny data()[132] 3.164s passed
seqGetAlphaCast data()[133] 3.166s passed
getOfSeqSingleton data()[134] 3.174s passed
getOfSeqSingletonConcrete data()[135] 3.163s passed
getOfSeqConcat data()[136] 3.182s passed
getOfSeqSub data()[137] 3.173s passed
getOfSeqReverse data()[138] 3.174s passed
lenOfSeqEmpty data()[139] 3.163s passed
div_unique2 data()[13] 3.311s passed
lenOfSeqSingleton data()[140] 3.173s passed
lenOfSeqConcat data()[141] 3.186s passed
lenOfSeqSub data()[142] 3.184s passed
lenOfSeqReverse data()[143] 3.199s passed
equalityToSeqGetAndSeqLenLeft data()[144] 3.171s passed
equalityToSeqGetAndSeqLenRight data()[145] 3.150s passed
getOfSeqSingletonEQ data()[146] 3.171s passed
getOfSeqConcatEQ data()[147] 3.180s passed
getOfSeqSubEQ data()[148] 3.166s passed
getOfSeqReverseEQ data()[149] 3.174s passed
div_exists data()[14] 3.375s passed
lenOfSeqEmptyEQ data()[150] 3.173s passed
lenOfSeqSingletonEQ data()[151] 3.169s passed
lenOfSeqConcatEQ data()[152] 3.163s passed
lenOfSeqSubEQ data()[153] 3.189s passed
lenOfSeqReverseEQ data()[154] 3.170s passed
getOfSeqDefEQ data()[155] 3.177s passed
lenOfSeqDefEQ data()[156] 3.168s passed
seqConcatWithSeqEmpty1 data()[157] 3.170s passed
seqConcatWithSeqEmpty2 data()[158] 3.176s passed
seqReverseOfSeqEmpty data()[159] 3.168s passed
div_one data()[15] 3.204s passed
subSeqComplete data()[160] 3.176s passed
subSeqTailR data()[161] 3.173s passed
subSeqTailL data()[162] 3.169s passed
subSeqTailEQR data()[163] 3.190s passed
subSeqTailEQL data()[164] 3.167s passed
seqDef_split data()[165] 3.192s passed
seqDef_induction_upper data()[166] 3.176s passed
seqDef_induction_upper_concrete data()[167] 3.182s passed
seqDef_induction_lower data()[168] 3.202s passed
seqDef_induction_lower_concrete data()[169] 3.203s passed
jdiv_one data()[16] 3.212s passed
seqDef_split_in_three data()[170] 3.206s passed
seqDef_empty data()[171] 3.176s passed
seqDef_one_summand data()[172] 3.195s passed
seqDef_lower_equals_upper data()[173] 3.172s passed
seqDefOfSeq data()[174] 3.182s passed
seqSelfDefinitionEQ2 data()[175] 3.174s passed
indexOfSeqSingleton data()[176] 3.179s passed
indexOfSeqConcatFirst data()[177] 3.180s passed
indexOfSeqConcatSecond data()[178] 3.180s passed
indexOfSeqSub data()[179] 3.197s passed
div_zero data()[17] 3.233s passed
lenOfArray2seq data()[180] 3.161s passed
getAnyOfArray2seq data()[181] 3.184s passed
getOfArray2seq data()[182] 3.168s passed
getAnyOfNPermInv data()[183] 3.195s passed
seqNPermRange data()[184] 3.222s passed
seqPermTrans data()[185] 3.224s passed
seqPermRefl data()[186] 3.187s passed
seqPermSplit data()[187] 3.186s passed
seqNPermRight data()[188] 3.241s passed
seqPermFromSwap data()[189] 3.215s passed
divResZero1 data()[18] 3.231s passed
seqPermTransAlt0 data()[190] 3.165s passed
seqPermTransAlt1 data()[191] 3.179s passed
seqPermTransAlt2 data()[192] 3.211s passed
seqPermTransAlt3 data()[193] 3.173s passed
seqPermForall data()[194] 3.291s passed
seqPermExists data()[195] 3.291s passed
schiffl_lemma_2 data()[196] 20.263s passed
schiffl_thm_1 data()[197] 3.960s passed
eqSameSeq data()[198] 3.353s passed
divResZero2 data()[19] 3.197s passed
eqTermCut data()[1] 3.794s passed
divResOne1 data()[20] 3.190s passed
divResOne2 data()[21] 3.215s passed
div_cancel1 data()[22] 3.190s passed
div_cancel2 data()[23] 3.198s passed
divAddMultDenom data()[24] 3.208s passed
divMinus data()[25] 3.235s passed
divMinusDenom data()[26] 3.222s passed
divLeastDPos data()[27] 3.163s passed
divLeastDNeg data()[28] 3.199s passed
divGreatestDPos data()[29] 3.173s passed
equivAllRight data()[2] 3.570s passed
divGreatestDNeg data()[30] 3.198s passed
divIncreasingPos data()[31] 3.215s passed
divIncreasingNeg data()[32] 3.183s passed
jdiv_zero data()[33] 3.175s passed
jdivPulloutMinusNum data()[34] 3.191s passed
jdivPulloutMinusDenom data()[35] 3.193s passed
jdiv_uniquePosPos data()[36] 3.238s passed
jdiv_uniquePosNeg data()[37] 3.262s passed
jdiv_uniqueNegPos data()[38] 3.171s passed
jdiv_uniqueNegNeg data()[39] 3.182s passed
irrflConcrete1 data()[3] 3.530s passed
jdivMultDenom1 data()[40] 3.187s passed
jdivMultDenom2 data()[41] 3.185s passed
mod_geZero data()[42] 3.170s passed
mod_lessDenom data()[43] 3.171s passed
jmod_NumPos data()[44] 3.186s passed
jmod_NumNeg data()[45] 3.191s passed
jmod_geZero data()[46] 3.153s passed
jmodNumZero data()[47] 3.183s passed
jmod_pulloutminusNum data()[48] 3.169s passed
jmod_pulloutminusDenom data()[49] 3.171s passed
irrflConcrete2 data()[4] 3.307s passed
jmodUnique1 data()[50] 3.208s passed
jmodUnique2 data()[51] 3.206s passed
intDivRem data()[52] 3.164s passed
jmodjmod data()[53] 3.185s passed
jmodDivisible data()[54] 3.203s passed
jmodDivisibleRep data()[55] 3.151s passed
jdivAddMultDenom data()[56] 3.247s passed
jmodAltZero data()[57] 3.182s passed
jmodAddMultDenomZero data()[58] 3.160s passed
polyDiv_zero data()[59] 3.192s passed
cancel_gtPos data()[5] 3.387s passed
polyMod_ltdivDenom data()[60] 3.170s passed
bsum_empty data()[61] 3.155s passed
bsum_induction_upper data()[62] 3.166s passed
bsum_induction_lower data()[63] 3.187s passed
bsum_num_of_bounds data()[64] 3.164s passed
bsum_num_of_bounds2 data()[65] 3.192s passed
bsum_induction_upper2 data()[66] 3.158s passed
bsum_induction_upper_concrete data()[67] 3.159s passed
bsum_induction_upper_concrete_2 data()[68] 3.159s passed
bsum_induction_upper2_concrete data()[69] 3.167s passed
cancel_gtNeg data()[6] 3.353s passed
bsum_induction_lower_concrete data()[70] 3.167s passed
bsum_induction_lower2 data()[71] 3.157s passed
bsum_induction_lower2_concrete data()[72] 3.155s passed
bsum_positive data()[73] 3.195s passed
bsum_upper_bound data()[74] 3.193s passed
bsum_lower_bound data()[75] 3.193s passed
bsum_positive_lower_bound_element data()[76] 3.182s passed
bsum_sub_same_index data()[77] 3.159s passed
bsum_less_same_index data()[78] 3.221s passed
bsum_equal_except_one_index data()[79] 3.173s passed
moduloIntIsInInt data()[7] 3.299s passed
bsum_num_of_is_max data()[80] 3.189s passed
bsum_num_of_is_max2 data()[81] 3.157s passed
bsum_num_of_is_max3 data()[82] 3.166s passed
bsum_num_of_is_max4 data()[83] 3.183s passed
bsum_num_of_lt_max data()[84] 3.157s passed
bsum_num_of_lt_max2 data()[85] 3.194s passed
bsum_num_of_lt_max3 data()[86] 3.167s passed
bsum_num_of_lt_max4 data()[87] 3.174s passed
bsum_num_of_gt0 data()[88] 3.177s passed
bsum_num_of_gt0_alt data()[89] 3.175s passed
moduloLongIsInLong data()[8] 3.282s passed
bsum_add_concrete data()[90] 3.172s passed
bprod_all_positive data()[91] 3.175s passed
bprod_split data()[92] 3.149s passed
powConcrete0 data()[93] 3.168s passed
powConcrete1 data()[94] 3.151s passed
powSplitFactor data()[95] 3.155s passed
powAdd data()[96] 3.172s passed
powMono data()[97] 3.155s passed
powMonoConcrete data()[98] 3.168s passed
powMonoConcreteRight data()[99] 3.152s passed
moduloShortIsInShort data()[9] 3.235s passed

Standard output

296        INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src/test/resources/testcase/dummyTrue.key 
315        DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 7.04ms 
541        INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
560        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)

1555       DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for Meta 
1557       DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for Meta 
1558       DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for Meta 
1558       DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for Meta 
2875       DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for JavaBigintExpression 
8116       DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 7.57s 
8183       INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof dummyTrue.key 
8214       DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 32.6ns 
8225       INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/firstOrder/Taclet_eqTermCut.proof 
8225       DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 170.4ns 
8234       INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
11067      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.83s 
11071      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: eqTermCut 
11985      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: eqTermCut 
12011      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 19.29ms 
12027      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/firstOrder/Taclet_equivAllRight.proof 
12027      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 181ns 
12030      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
14717      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.69s 
14717      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: equivAllRight 
15571      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: equivAllRight 
15592      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 14.93ms 
15597      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_irrflConcrete1.proof 
15597      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 222.2ns 
15600      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
18262      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.66s 
18262      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: irrflConcrete1 
19120      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: irrflConcrete1 
19125      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.55ms 
19127      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_irrflConcrete2.proof 
19128      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 129.9ns 
19129      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
21603      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.47s 
21603      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: irrflConcrete2 
22427      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: irrflConcrete2 
22432      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.36ms 
22435      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_cancel_gtPos.proof 
22435      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 445.5ns 
22436      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
24916      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.48s 
24916      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: cancel_gtPos 
25782      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: cancel_gtPos 
25819      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 33.91ms 
25820      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_cancel_gtNeg.proof 
25821      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 143.2ns 
25822      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
28304      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.48s 
28305      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: cancel_gtNeg 
29140      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: cancel_gtNeg 
29172      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 28.17ms 
29176      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intRulesIgnoringOF/Taclet_moduloIntIsInInt.proof 
29176      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 344.9ns 
29177      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
31651      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.47s 
31651      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: moduloIntIsInInt 
32469      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: moduloIntIsInInt 
32473      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 731.39ns 
32474      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intRulesIgnoringOF/Taclet_moduloLongIsInLong.proof 
32475      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 192.4ns 
32477      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
34938      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.46s 
34939      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: moduloLongIsInLong 
35753      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: moduloLongIsInLong 
35756      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 626.89ns 
35757      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intRulesIgnoringOF/Taclet_moduloShortIsInShort.proof 
35758      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 183.1ns 
35759      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
38172      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.41s 
38173      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: moduloShortIsInShort 
38983      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: moduloShortIsInShort 
38986      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 577ns 
38992      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intRulesIgnoringOF/Taclet_moduloByteIsInByte.proof 
38993      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 322.5ns 
38995      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
41440      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.45s 
41440      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: moduloByteIsInByte 
42233      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: moduloByteIsInByte 
42236      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 534.39ns 
42238      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intRulesIgnoringOF/Taclet_moduloCharIsInChar.proof 
42239      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 305.3ns 
42240      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
44641      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.4s 
44642      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: moduloCharIsInChar 
45433      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: moduloCharIsInChar 
45436      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 660.69ns 
45438      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_div_unique1.proof 
45438      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 321.4ns 
45439      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
47880      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.44s 
47881      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: div_unique1 
48673      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: div_unique1 
48710      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 33.75ms 
48712      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_div_unique2.proof 
48712      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 153.4ns 
48713      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
51149      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.44s 
51150      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: div_unique2 
51966      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: div_unique2 
52018      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 48.52ms 
52023      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_div_exists.proof 
52023      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 134.8ns 
52025      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
54438      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.41s 
54438      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: div_exists 
55241      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: div_exists 
55396      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 145.93ms 
55398      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_div_one.proof 
55399      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 131.1ns 
55399      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
57823      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.42s 
57824      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: div_one 
58597      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: div_one 
58601      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.25ms 
58602      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdiv_one.proof 
58603      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 85.3ns 
58603      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
61010      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.41s 
61010      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdiv_one 
61810      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdiv_one 
61813      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.17ms 
61815      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_div_zero.proof 
61815      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 85.9ns 
61816      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
64199      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.38s 
64199      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: div_zero 
65005      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: div_zero 
65045      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 36.05ms 
65049      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divResZero1.proof 
65050      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 340.7ns 
65051      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
67477      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.43s 
67478      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divResZero1 
68266      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divResZero1 
68278      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 8.44ms 
68280      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divResZero2.proof 
68280      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 177.3ns 
68281      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
70672      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.39s 
70672      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divResZero2 
71464      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divResZero2 
71475      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 7.95ms 
71476      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divResOne1.proof 
71476      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 115.7ns 
71477      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
73885      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.41s 
73885      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divResOne1 
74654      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divResOne1 
74665      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 8.64ms 
74667      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divResOne2.proof 
74667      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 103.7ns 
74668      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
77079      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.41s 
77080      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divResOne2 
77870      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divResOne2 
77880      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 7.9ms 
77882      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_div_cancel1.proof 
77882      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 104.8ns 
77882      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
80266      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.38s 
80266      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: div_cancel1 
81054      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: div_cancel1 
81070      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 12.98ms 
81072      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_div_cancel2.proof 
81072      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 120.4ns 
81073      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
83479      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.41s 
83479      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: div_cancel2 
84265      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: div_cancel2 
84268      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.19ms 
84269      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divAddMultDenom.proof 
84269      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 99.6ns 
84270      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
86660      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.39s 
86660      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divAddMultDenom 
87447      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divAddMultDenom 
87476      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 24.18ms 
87478      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divMinus.proof 
87478      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 117.9ns 
87479      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
89901      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.42s 
89902      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divMinus 
90669      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divMinus 
90711      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 34.79ms 
90713      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divMinusDenom.proof 
90714      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 292.4ns 
90715      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
93122      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.41s 
93122      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divMinusDenom 
93907      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divMinusDenom 
93933      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 21.2ms 
93934      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divLeastDPos.proof 
93935      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 97.5ns 
93935      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
96308      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.37s 
96308      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divLeastDPos 
97091      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divLeastDPos 
97097      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.92ms 
97098      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divLeastDNeg.proof 
97098      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 88.5ns 
97099      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
99490      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.39s 
99491      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divLeastDNeg 
100259     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divLeastDNeg 
100295     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 33.61ms 
100297     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divGreatestDPos.proof 
100297     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 84.1ns 
100298     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
102676     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.38s 
102676     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divGreatestDPos 
103460     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divGreatestDPos 
103469     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 6.3ms 
103470     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divGreatestDNeg.proof 
103470     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 86.9ns 
103471     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
105845     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.37s 
105845     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divGreatestDNeg 
106659     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divGreatestDNeg 
106666     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.36ms 
106671     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divIncreasingPos.proof 
106673     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 2.73ms 
106675     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
109089     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.41s 
109090     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divIncreasingPos 
109877     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divIncreasingPos 
109883     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.83ms 
109885     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divIncreasingNeg.proof 
109886     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 280.1ns 
109886     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
112276     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.39s 
112277     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divIncreasingNeg 
113061     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divIncreasingNeg 
113066     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.49ms 
113067     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdiv_zero.proof 
113068     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 85.5ns 
113068     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
115473     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.4s 
115473     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdiv_zero 
116238     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdiv_zero 
116241     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.22ms 
116243     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdivPulloutMinusNum.proof 
116243     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 88.8ns 
116244     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
118640     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.4s 
118640     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdivPulloutMinusNum 
119425     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdivPulloutMinusNum 
119432     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 5.78ms 
119434     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdivPulloutMinusDenom.proof 
119434     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 97.1ns 
119435     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
121812     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.38s 
121812     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdivPulloutMinusDenom 
122598     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdivPulloutMinusDenom 
122626     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 22.71ms 
122627     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdiv_uniquePosPos.proof 
122627     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 159.5ns 
122628     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
125066     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.44s 
125066     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdiv_uniquePosPos 
125850     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdiv_uniquePosPos 
125863     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 9.59ms 
125865     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdiv_uniquePosNeg.proof 
125865     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 165.5ns 
125866     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
128254     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.39s 
128254     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdiv_uniquePosNeg 
129113     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdiv_uniquePosNeg 
129125     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 9.54ms 
129127     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdiv_uniqueNegPos.proof 
129127     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 92.2ns 
129128     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
131518     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.39s 
131519     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdiv_uniqueNegPos 
132283     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdiv_uniqueNegPos 
132296     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 9.6ms 
132297     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdiv_uniqueNegNeg.proof 
132297     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 91.4ns 
132298     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
134682     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.38s 
134682     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdiv_uniqueNegNeg 
135466     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdiv_uniqueNegNeg 
135479     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 10.19ms 
135481     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdivMultDenom1.proof 
135481     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 249.2ns 
135482     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
137856     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.37s 
137856     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdivMultDenom1 
138638     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdivMultDenom1 
138664     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 21.97ms 
138667     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdivMultDenom2.proof 
138667     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 279.2ns 
138668     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
141060     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.39s 
141061     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdivMultDenom2 
141847     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdivMultDenom2 
141850     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 827.09ns 
141852     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_mod_geZero.proof 
141852     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 249ns 
141853     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
144236     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.38s 
144236     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: mod_geZero 
145017     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: mod_geZero 
145021     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.81ms 
145022     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_mod_lessDenom.proof 
145022     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 80.7ns 
145023     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
147398     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.38s 
147399     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: mod_lessDenom 
148185     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: mod_lessDenom 
148191     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.88ms 
148193     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmod_NumPos.proof 
148194     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 905.39ns 
148195     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
150586     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.39s 
150586     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmod_NumPos 
151371     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmod_NumPos 
151377     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.43ms 
151379     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmod_NumNeg.proof 
151379     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 84.1ns 
151379     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
153752     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.37s 
153752     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmod_NumNeg 
154544     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmod_NumNeg 
154569     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 21.55ms 
154570     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmod_geZero.proof 
154570     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 90.9ns 
154571     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
156955     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.38s 
156956     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmod_geZero 
157716     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmod_geZero 
157722     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.11ms 
157723     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmodNumZero.proof 
157723     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 72ns 
157724     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
160111     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.39s 
160112     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmodNumZero 
160900     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmodNumZero 
160904     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.61ms 
160906     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmod_pulloutminusNum.proof 
160906     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 259.3ns 
160907     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
163283     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.38s 
163283     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmod_pulloutminusNum 
164070     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmod_pulloutminusNum 
164073     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.13ms 
164075     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmod_pulloutminusDenom.proof 
164075     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 198.5ns 
164076     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
166461     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.38s 
166461     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmod_pulloutminusDenom 
167241     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmod_pulloutminusDenom 
167244     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.32ms 
167246     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmodUnique1.proof 
167246     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 78.8ns 
167247     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
169623     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.38s 
169623     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmodUnique1 
170404     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmodUnique1 
170452     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 40.09ms 
170454     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmodUnique2.proof 
170454     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 148.7ns 
170455     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
172842     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.39s 
172842     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmodUnique2 
173602     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmodUnique2 
173658     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 48.39ms 
173660     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_intDivRem.proof 
173660     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 84.2ns 
173661     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
176042     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.38s 
176043     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: intDivRem 
176820     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: intDivRem 
176822     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1ms 
176823     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmodjmod.proof 
176824     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 142.4ns 
176824     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
179192     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.37s 
179192     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmodjmod 
179972     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmodjmod 
180006     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 30.69ms 
180010     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmodDivisible.proof 
180015     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 4.94ms 
180016     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
182411     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.39s 
182411     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmodDivisible 
183191     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmodDivisible 
183210     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 16.12ms 
183211     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmodDivisibleRep.proof 
183211     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 83.1ns 
183212     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
185580     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.37s 
185580     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmodDivisibleRep 
186360     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmodDivisibleRep 
186362     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 828.99ns 
186363     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdivAddMultDenom.proof 
186363     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 63.4ns 
186364     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
188753     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.39s 
188755     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdivAddMultDenom 
189517     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdivAddMultDenom 
189607     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 79.87ms 
189610     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmodAltZero.proof 
189610     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 222.7ns 
189611     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
192004     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.39s 
192004     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmodAltZero 
192782     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmodAltZero 
192790     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 5.93ms 
192791     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmodAddMultDenomZero.proof 
192791     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 70ns 
192792     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
195163     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.37s 
195164     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmodAddMultDenomZero 
195944     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmodAddMultDenomZero 
195950     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.4ms 
195951     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_polyDiv_zero.proof 
195951     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 74.6ns 
195952     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
198345     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.39s 
198345     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: polyDiv_zero 
199130     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: polyDiv_zero 
199143     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 10.25ms 
199144     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_polyMod_ltdivDenom.proof 
199144     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 134.4ns 
199145     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
201518     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.37s 
201519     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: polyMod_ltdivDenom 
202301     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: polyMod_ltdivDenom 
202311     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 5.04ms 
202314     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_empty.proof 
202314     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 132.7ns 
202315     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
204687     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.37s 
204687     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_empty 
205464     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_empty 
205468     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.29ms 
205469     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_induction_upper.proof 
205469     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 121.9ns 
205470     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
207848     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.38s 
207848     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_upper 
208630     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_induction_upper 
208633     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.64ms 
208634     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_induction_lower.proof 
208634     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 56.8ns 
208635     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
211028     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.39s 
211028     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_lower 
211808     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_induction_lower 
211821     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 10.15ms 
211822     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_bounds.proof 
211822     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 67.1ns 
211823     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
214211     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.39s 
214211     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_bounds 
214973     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_bounds 
214984     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 8.43ms 
214985     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_bounds2.proof 
214985     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 72.6ns 
214986     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
217378     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.39s 
217378     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_bounds2 
218163     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_bounds2 
218176     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 10.99ms 
218178     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_induction_upper2.proof 
218179     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 219.2ns 
218180     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
220552     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.37s 
220552     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_upper2 
221332     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_induction_upper2 
221334     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 816.39ns 
221335     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_induction_upper_concrete.proof 
221336     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 65.7ns 
221336     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
223715     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.38s 
223715     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_upper_concrete 
224491     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_induction_upper_concrete 
224494     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.16ms 
224495     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_induction_upper_concrete_2.proof 
224495     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 62.3ns 
224495     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
226865     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.37s 
226865     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_upper_concrete_2 
227648     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_induction_upper_concrete_2 
227653     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.44ms 
227654     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_induction_upper2_concrete.proof 
227654     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 63.3ns 
227655     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
230050     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.4s 
230051     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_upper2_concrete 
230817     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_induction_upper2_concrete 
230819     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 818.99ns 
230820     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_induction_lower_concrete.proof 
230820     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 71ns 
230821     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
233205     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.38s 
233205     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_lower_concrete 
233984     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_induction_lower_concrete 
233986     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 606.29ns 
233988     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_induction_lower2.proof 
233988     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 60.6ns 
233988     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
236361     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.37s 
236361     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_lower2 
237141     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_induction_lower2 
237144     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.54ms 
237145     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_induction_lower2_concrete.proof 
237145     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 73.4ns 
237146     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
239538     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.39s 
239538     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_lower2_concrete 
240296     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_induction_lower2_concrete 
240298     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 711.29ns 
240300     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_positive.proof 
240300     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 105.2ns 
240301     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
242678     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.38s 
242679     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_positive 
243461     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_positive 
243493     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 29.31ms 
243495     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_upper_bound.proof 
243495     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 240.4ns 
243496     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
245880     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.38s 
245880     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_upper_bound 
246659     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_upper_bound 
246687     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 24.87ms 
246688     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_lower_bound.proof 
246688     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 73.1ns 
246689     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
249073     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.38s 
249073     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_lower_bound 
249852     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_lower_bound 
249879     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 24.11ms 
249882     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_positive_lower_bound_element.proof 
249882     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 411.5ns 
249883     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
252251     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.37s 
252252     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_positive_lower_bound_element 
253032     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_positive_lower_bound_element 
253061     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 25.1ms 
253063     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_sub_same_index.proof 
253063     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 209.6ns 
253064     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
255443     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.38s 
255443     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_sub_same_index 
256202     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_sub_same_index 
256220     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 15.22ms 
256221     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_less_same_index.proof 
256221     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 73.5ns 
256222     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
258627     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.4s 
258627     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_less_same_index 
259410     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_less_same_index 
259441     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 27.38ms 
259443     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_equal_except_one_index.proof 
259444     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 198.9ns 
259444     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
261815     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.37s 
261815     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_equal_except_one_index 
262596     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_equal_except_one_index 
262614     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 15.09ms 
262615     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_is_max.proof 
262616     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 74.1ns 
262616     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
265014     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.4s 
265014     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_is_max 
265790     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_is_max 
265803     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 10.55ms 
265804     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_is_max2.proof 
265805     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 66.3ns 
265805     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
268163     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.36s 
268163     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_is_max2 
268946     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_is_max2 
268960     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 11.4ms 
268961     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_is_max3.proof 
268961     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 67.1ns 
268962     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
271355     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.39s 
271355     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_is_max3 
272114     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_is_max3 
272126     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 9.43ms 
272127     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_is_max4.proof 
272127     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 70.2ns 
272128     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
274516     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.39s 
274516     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_is_max4 
275294     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_is_max4 
275309     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 12.51ms 
275311     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_lt_max.proof 
275311     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 69ns 
275311     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
277674     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.36s 
277674     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_lt_max 
278452     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_lt_max 
278467     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 11.78ms 
278468     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_lt_max2.proof 
278468     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 74.9ns 
278469     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
280858     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.39s 
280858     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_lt_max2 
281635     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_lt_max2 
281659     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 15.96ms 
281662     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_lt_max3.proof 
281662     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 181.1ns 
281664     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
284034     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.37s 
284034     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_lt_max3 
284814     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_lt_max3 
284828     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 11.45ms 
284829     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_lt_max4.proof 
284829     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 72ns 
284830     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
287221     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.39s 
287221     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_lt_max4 
287986     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_lt_max4 
288001     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 12.84ms 
288002     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_gt0.proof 
288002     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 62ns 
288003     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
290380     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.38s 
290380     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_gt0 
291159     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_gt0 
291178     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 16.35ms 
291180     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_gt0_alt.proof 
291181     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 199.6ns 
291181     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
293558     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.38s 
293558     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_gt0_alt 
294338     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_gt0_alt 
294353     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 12.56ms 
294354     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_add_concrete.proof 
294354     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 69.4ns 
294355     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
296755     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.4s 
296756     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_add_concrete 
297520     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_add_concrete 
297525     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.69ms 
297526     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bprod/Taclet_bprod_all_positive.proof 
297526     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 48.2ns 
297527     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
299910     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.38s 
299910     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bprod_all_positive 
300690     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bprod_all_positive 
300700     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 8.12ms 
300701     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bprod/Taclet_bprod_split.proof 
300701     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 50ns 
300702     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
303067     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.36s 
303067     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bprod_split 
303846     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bprod_split 
303850     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.68ms 
303851     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powConcrete0.proof 
303851     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 55.8ns 
303851     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
306235     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.38s 
306235     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powConcrete0 
307015     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powConcrete0 
307017     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 536.79ns 
307018     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powConcrete1.proof 
307018     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 57.6ns 
307019     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
309387     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.37s 
309387     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powConcrete1 
310166     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powConcrete1 
310168     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 626.6ns 
310170     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powSplitFactor.proof 
310170     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 79.9ns 
310170     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
312558     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.39s 
312558     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powSplitFactor 
313319     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powSplitFactor 
313324     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.02ms 
313325     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powAdd.proof 
313325     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 59.9ns 
313326     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
315709     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.38s 
315709     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powAdd 
316490     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powAdd 
316495     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.86ms 
316497     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powMono.proof 
316497     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 168.3ns 
316498     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
318861     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.36s 
318861     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powMono 
319642     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powMono 
319650     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 6.66ms 
319651     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powMonoConcrete.proof 
319652     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 52.2ns 
319652     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
322035     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.38s 
322035     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powMonoConcrete 
322815     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powMonoConcrete 
322818     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.43ms 
322819     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powMonoConcreteRight.proof 
322819     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 49.2ns 
322820     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
325188     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.37s 
325188     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powMonoConcreteRight 
325969     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powMonoConcreteRight 
325971     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 400.8ns 
325972     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powPositive.proof 
325972     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 59.2ns 
325973     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
328357     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.38s 
328357     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powPositive 
329118     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powPositive 
329122     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.54ms 
329123     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powPositiveConcrete.proof 
329123     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 59.3ns 
329124     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
331502     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.38s 
331502     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powPositiveConcrete 
332283     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powPositiveConcrete 
332285     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 468.6ns 
332286     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powGeq1Concrete.proof 
332286     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 47.9ns 
332287     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
334648     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.36s 
334648     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powGeq1Concrete 
335427     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powGeq1Concrete 
335429     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 485.1ns 
335430     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_pow2InIntLower.proof 
335430     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 47.4ns 
335431     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
337814     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.38s 
337814     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: pow2InIntLower 
338576     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: pow2InIntLower 
338579     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 514.6ns 
338580     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_pow2InIntUpper.proof 
338580     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 171.1ns 
338581     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
340964     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.38s 
340965     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: pow2InIntUpper 
341747     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: pow2InIntUpper 
341750     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.61ms 
341751     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logSelfConcrete.proof 
341751     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 60.2ns 
341752     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
344124     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.37s 
344124     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logSelfConcrete 
344909     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logSelfConcrete 
344922     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 9.26ms 
344924     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_log1Concrete.proof 
344924     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 68.6ns 
344925     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
347307     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.38s 
347307     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: log1Concrete 
348087     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: log1Concrete 
348091     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.44ms 
348093     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logProduct.proof 
348093     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 161.5ns 
348098     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
350473     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.37s 
350473     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logProduct 
351254     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logProduct 
351259     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.24ms 
351260     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logTimesBaseConcrete.proof 
351261     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 50.2ns 
351261     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
353650     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.39s 
353650     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logTimesBaseConcrete 
354429     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logTimesBaseConcrete 
354432     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.75ms 
354433     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logProdIdentity.proof 
354433     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 66ns 
354434     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
356808     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.37s 
356808     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logProdIdentity 
357604     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logProdIdentity 
357616     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 8.86ms 
357618     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logProdIdentityConcrete.proof 
357618     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 185.8ns 
357619     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
360019     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.4s 
360019     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logProdIdentityConcrete 
360811     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logProdIdentityConcrete 
360814     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.42ms 
360815     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logPowIdentity.proof 
360815     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 58.4ns 
360816     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
363249     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.43s 
363249     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logPowIdentity 
364027     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logPowIdentity 
364030     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 868.89ns 
364031     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logPowIdentityConcrete.proof 
364031     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 70.4ns 
364032     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
366415     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.38s 
366415     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logPowIdentityConcrete 
367176     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logPowIdentityConcrete 
367180     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.58ms 
367181     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logPositive.proof 
367181     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 56.6ns 
367181     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
369560     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.38s 
369560     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logPositive 
370339     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logPositive 
370351     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 9.45ms 
370352     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logPositiveConcrete.proof 
370352     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 62.1ns 
370353     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
372734     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.38s 
372735     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logPositiveConcrete 
373497     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logPositiveConcrete 
373501     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 310.2ns 
373502     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logMono.proof 
373503     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 61.1ns 
373503     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
375875     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.37s 
375875     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logMono 
376653     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logMono 
376680     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 22.83ms 
376681     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logMonoConcrete.proof 
376681     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 68.9ns 
376682     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
379065     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.38s 
379065     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logMonoConcrete 
379825     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logMonoConcrete 
379828     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.25ms 
379829     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powLogLess.proof 
379829     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 53.4ns 
379830     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
382213     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.38s 
382213     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powLogLess 
382993     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powLogLess 
383007     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 11.15ms 
383015     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powLogMore2.proof 
383016     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 227.7ns 
383016     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
385422     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.41s 
385422     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powLogMore2 
386184     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powLogMore2 
386197     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 10.49ms 
386198     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logLessThanPow.proof 
386198     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 64.7ns 
386199     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
388586     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.39s 
388586     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logLessThanPow 
389364     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logLessThanPow 
389386     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 18.83ms 
389388     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logLessThanPowConcrete.proof 
389388     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 183.5ns 
389389     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
391773     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.38s 
391773     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logLessThanPowConcrete 
392553     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logLessThanPowConcrete 
392556     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 540.6ns 
392557     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logSqueeze.proof 
392557     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 57.5ns 
392557     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
394928     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.37s 
394928     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logSqueeze 
395707     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logSqueeze 
395711     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.91ms 
395712     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/booleanRules/Taclet_ifthenelse_equals.proof 
395712     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 51.5ns 
395713     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
398102     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.39s 
398102     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: ifthenelse_equals 
398905     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: ifthenelse_equals 
398908     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.19ms 
398909     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/booleanRules/Taclet_ifthenelse_equals_1.proof 
398910     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 59.8ns 
398911     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
401362     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.45s 
401362     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: ifthenelse_equals_1 
402178     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: ifthenelse_equals_1 
402180     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 644.1ns 
402181     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/booleanRules/Taclet_ifthenelse_equals_2.proof 
402181     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 51.6ns 
402182     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
404649     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.47s 
404649     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: ifthenelse_equals_2 
405446     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: ifthenelse_equals_2 
405448     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 608.29ns 
405452     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/locSet/Taclet_disjointWithSingleton1.proof 
405452     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 60.9ns 
405453     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
407845     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.39s 
407845     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: disjointWithSingleton1 
408637     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: disjointWithSingleton1 
408639     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 978.09ns 
408640     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/locSet/Taclet_disjointWithSingleton2.proof 
408640     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 50.7ns 
408641     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
411009     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.37s 
411010     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: disjointWithSingleton2 
411794     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: disjointWithSingleton2 
411796     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 865.09ns 
411799     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/locSet/Taclet_disjointArrayRanges.proof 
411800     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 1.33ms 
411803     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
414187     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.38s 
414187     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: disjointArrayRanges 
414968     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: disjointArrayRanges 
414975     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 5.17ms 
414977     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/locSet/Taclet_disjointArrayRangeAllFields1.proof 
414977     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 46.8ns 
414977     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
417351     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.37s 
417351     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: disjointArrayRangeAllFields1 
418117     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: disjointArrayRangeAllFields1 
418124     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.54ms 
418125     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/locSet/Taclet_disjointArrayRangeAllFields2.proof 
418125     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 50ns 
418126     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
420510     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.38s 
420510     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: disjointArrayRangeAllFields2 
421299     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: disjointArrayRangeAllFields2 
421305     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.59ms 
421307     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqSelfDefinition.proof 
421307     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 68.3ns 
421308     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
423688     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.38s 
423688     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqSelfDefinition 
424474     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqSelfDefinition 
424485     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 9.25ms 
424486     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqOutsideValue.proof 
424487     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 175.2ns 
424487     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
426869     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.38s 
426869     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqOutsideValue 
427638     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqOutsideValue 
427641     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.76ms 
427643     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_castedGetAny.proof 
427643     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 56.2ns 
427643     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
430017     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.37s 
430017     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: castedGetAny 
430802     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: castedGetAny 
430805     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.02ms 
430806     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqGetAlphaCast.proof 
430806     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 48.2ns 
430807     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
433177     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.37s 
433178     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqGetAlphaCast 
433970     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqGetAlphaCast 
433972     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 594.39ns 
433973     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqSingleton.proof 
433973     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 50.3ns 
433973     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
436357     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.38s 
436357     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqSingleton 
437144     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqSingleton 
437146     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 757.09ns 
437147     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqSingletonConcrete.proof 
437147     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 53.7ns 
437147     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
439535     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.39s 
439535     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqSingletonConcrete 
440307     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqSingletonConcrete 
440309     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 724.39ns 
440310     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqConcat.proof 
440310     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 58.7ns 
440310     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
442694     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.38s 
442694     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqConcat 
443483     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqConcat 
443491     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 5.72ms 
443492     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqSub.proof 
443492     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 48.4ns 
443492     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
445874     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.38s 
445874     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqSub 
446661     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqSub 
446664     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.09ms 
446665     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqReverse.proof 
446665     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 47.5ns 
446665     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
449045     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.38s 
449046     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqReverse 
449833     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqReverse 
449838     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.25ms 
449839     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqEmpty.proof 
449839     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 54.3ns 
449839     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
452228     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.39s 
452228     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqEmpty 
452998     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqEmpty 
453000     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 756.79ns 
453002     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqSingleton.proof 
453002     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 58.6ns 
453002     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
455382     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.38s 
455382     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqSingleton 
456171     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqSingleton 
456173     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 594.6ns 
456174     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqConcat.proof 
456174     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 61.7ns 
456175     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
458564     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.39s 
458565     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqConcat 
459357     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqConcat 
459360     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.28ms 
459361     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqSub.proof 
459363     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 2.03ms 
459364     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
461752     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.39s 
461752     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqSub 
462541     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqSub 
462543     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 731.49ns 
462544     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqReverse.proof 
462544     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 48.8ns 
462545     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
464953     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.41s 
464953     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqReverse 
465740     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqReverse 
465742     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 923.99ns 
465743     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_equalityToSeqGetAndSeqLenLeft.proof 
465743     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 55.2ns 
465744     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
468121     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.38s 
468121     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: equalityToSeqGetAndSeqLenLeft 
468909     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: equalityToSeqGetAndSeqLenLeft 
468914     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.45ms 
468915     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_equalityToSeqGetAndSeqLenRight.proof 
468915     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 56.7ns 
468916     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
471293     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.38s 
471293     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: equalityToSeqGetAndSeqLenRight 
472060     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: equalityToSeqGetAndSeqLenRight 
472064     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.82ms 
472065     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqSingletonEQ.proof 
472065     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 45.3ns 
472065     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
474447     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.38s 
474447     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqSingletonEQ 
475232     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqSingletonEQ 
475235     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 734.09ns 
475236     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqConcatEQ.proof 
475236     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 53.1ns 
475236     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
477618     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.38s 
477618     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqConcatEQ 
478406     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqConcatEQ 
478414     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 5.73ms 
478415     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqSubEQ.proof 
478415     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 59.6ns 
478416     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
480790     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.37s 
480790     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqSubEQ 
481579     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqSubEQ 
481580     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 467.6ns 
481581     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqReverseEQ.proof 
481582     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 56ns 
481582     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
483962     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.38s 
483962     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqReverseEQ 
484750     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqReverseEQ 
484755     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.3ms 
484756     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqEmptyEQ.proof 
484756     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 50.8ns 
484757     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
487136     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.38s 
487137     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqEmptyEQ 
487926     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqEmptyEQ 
487928     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 742.69ns 
487929     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqSingletonEQ.proof 
487929     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 46.9ns 
487929     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
490307     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.38s 
490307     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqSingletonEQ 
491094     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqSingletonEQ 
491097     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 587.39ns 
491098     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqConcatEQ.proof 
491098     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 44.8ns 
491098     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
493471     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.37s 
493471     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqConcatEQ 
494256     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqConcatEQ 
494260     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.7ms 
494261     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqSubEQ.proof 
494261     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 43.3ns 
494261     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
496654     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.39s 
496654     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqSubEQ 
497446     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqSubEQ 
497448     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 754.89ns 
497449     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqReverseEQ.proof 
497449     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 59ns 
497450     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
499828     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.38s 
499828     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqReverseEQ 
500616     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqReverseEQ 
500618     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.18ms 
500619     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqDefEQ.proof 
500619     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 53.8ns 
500620     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
503003     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.38s 
503004     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqDefEQ 
503793     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqDefEQ 
503796     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 911.39ns 
503798     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqDefEQ.proof 
503798     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 45.7ns 
503799     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
506175     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.38s 
506175     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqDefEQ 
506961     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqDefEQ 
506964     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.88ms 
506965     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqConcatWithSeqEmpty1.proof 
506965     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 51.1ns 
506966     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
509339     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.37s 
509340     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqConcatWithSeqEmpty1 
510127     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqConcatWithSeqEmpty1 
510134     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 5.18ms 
510136     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqConcatWithSeqEmpty2.proof 
510136     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 45.2ns 
510136     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
512511     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.38s 
512511     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqConcatWithSeqEmpty2 
513302     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqConcatWithSeqEmpty2 
513310     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 5.88ms 
513312     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqReverseOfSeqEmpty.proof 
513312     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 159.7ns 
513312     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
515688     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.38s 
515688     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqReverseOfSeqEmpty 
516473     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqReverseOfSeqEmpty 
516479     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.83ms 
516480     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_subSeqComplete.proof 
516480     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 50.8ns 
516480     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
518856     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.38s 
518856     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: subSeqComplete 
519646     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: subSeqComplete 
519654     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 6.94ms 
519656     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_subSeqTailR.proof 
519656     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 157.5ns 
519657     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
522029     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.37s 
522030     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: subSeqTailR 
522818     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: subSeqTailR 
522827     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 7.22ms 
522828     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_subSeqTailL.proof 
522828     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 55.4ns 
522829     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
525198     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.37s 
525198     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: subSeqTailL 
525987     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: subSeqTailL 
525996     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 7.26ms 
525997     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_subSeqTailEQR.proof 
525997     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 62.7ns 
525998     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
528390     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.39s 
528390     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: subSeqTailEQR 
529178     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: subSeqTailEQR 
529187     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 6.61ms 
529188     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_subSeqTailEQL.proof 
529188     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 51ns 
529189     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
531560     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.37s 
531560     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: subSeqTailEQL 
532347     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: subSeqTailEQL 
532353     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.55ms 
532354     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDef_split.proof 
532354     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 55.7ns 
532355     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
534738     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.38s 
534739     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_split 
535527     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDef_split 
535545     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 15.31ms 
535546     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDef_induction_upper.proof 
535547     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 47.9ns 
535547     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
537915     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.37s 
537915     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_induction_upper 
538702     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDef_induction_upper 
538722     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 16.47ms 
538723     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDef_induction_upper_concrete.proof 
538723     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 58.5ns 
538724     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
541096     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.37s 
541096     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_induction_upper_concrete 
541886     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDef_induction_upper_concrete 
541904     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 15.12ms 
541905     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDef_induction_lower.proof 
541905     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 61.4ns 
541906     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
544299     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.39s 
544299     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_induction_lower 
545088     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDef_induction_lower 
545105     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 14.31ms 
545107     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDef_induction_lower_concrete.proof 
545107     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 61.8ns 
545107     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
547502     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.4s 
547503     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_induction_lower_concrete 
548291     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDef_induction_lower_concrete 
548308     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 14.64ms 
548309     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDef_split_in_three.proof 
548309     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 47.3ns 
548310     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
550678     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.37s 
550678     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_split_in_three 
551470     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDef_split_in_three 
551514     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 37.62ms 
551516     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDef_empty.proof 
551516     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 58.7ns 
551517     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
553894     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.38s 
553894     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_empty 
554684     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDef_empty 
554689     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.28ms 
554691     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDef_one_summand.proof 
554691     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 48ns 
554692     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
557069     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.38s 
557069     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_one_summand 
557858     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDef_one_summand 
557885     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.74ms 
557887     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDef_lower_equals_upper.proof 
557887     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 69.2ns 
557887     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
560264     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.38s 
560264     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_lower_equals_upper 
561054     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDef_lower_equals_upper 
561057     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.69ms 
561058     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDefOfSeq.proof 
561058     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 53.3ns 
561059     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
563438     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.38s 
563438     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDefOfSeq 
564228     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDefOfSeq 
564240     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 8.99ms 
564241     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqSelfDefinitionEQ2.proof 
564241     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 59.3ns 
564241     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
566621     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.38s 
566621     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqSelfDefinitionEQ2 
567408     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqSelfDefinitionEQ2 
567413     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.79ms 
567414     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_indexOfSeqSingleton.proof 
567414     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 44.8ns 
567415     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
569805     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.39s 
569805     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: indexOfSeqSingleton 
570590     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: indexOfSeqSingleton 
570593     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.17ms 
570594     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_indexOfSeqConcatFirst.proof 
570594     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 55.5ns 
570595     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
572975     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.38s 
572975     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: indexOfSeqConcatFirst 
573763     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: indexOfSeqConcatFirst 
573772     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 6.95ms 
573773     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_indexOfSeqConcatSecond.proof 
573773     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 53ns 
573774     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
576153     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.38s 
576153     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: indexOfSeqConcatSecond 
576943     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: indexOfSeqConcatSecond 
576952     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 7.41ms 
576953     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_indexOfSeqSub.proof 
576954     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 58.4ns 
576954     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
579351     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.4s 
579351     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: indexOfSeqSub 
580137     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: indexOfSeqSub 
580149     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 9.56ms 
580151     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfArray2seq.proof 
580151     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 175.7ns 
580152     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
582521     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.37s 
582521     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfArray2seq 
583308     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfArray2seq 
583311     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 871.39ns 
583312     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getAnyOfArray2seq.proof 
583312     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 43.8ns 
583312     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
585703     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.39s 
585704     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getAnyOfArray2seq 
586491     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getAnyOfArray2seq 
586494     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.46ms 
586495     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfArray2seq.proof 
586495     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 55.1ns 
586496     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
588871     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.38s 
588871     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfArray2seq 
589657     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfArray2seq 
589662     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.71ms 
589663     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_getAnyOfNPermInv.proof 
589663     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 46.4ns 
589664     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
592066     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.4s 
592066     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getAnyOfNPermInv 
592854     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getAnyOfNPermInv 
592858     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.52ms 
592859     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqNPermRange.proof 
592859     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 43.7ns 
592860     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
595236     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.38s 
595236     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqNPermRange 
596040     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqNPermRange 
596079     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 33.59ms 
596080     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermTrans.proof 
596080     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 58.1ns 
596081     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
598497     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.42s 
598497     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermTrans 
599286     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermTrans 
599303     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 13.39ms 
599305     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermRefl.proof 
599305     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 177.3ns 
599305     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
601694     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.39s 
601694     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermRefl 
602480     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermRefl 
602491     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 8.14ms 
602492     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermSplit.proof 
602492     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 61.5ns 
602492     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
604889     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.4s 
604889     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermSplit 
605674     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermSplit 
605676     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 148.8ns 
605677     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqNPermRight.proof 
605677     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 45.7ns 
605678     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
608055     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.38s 
608055     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqNPermRight 
608844     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqNPermRight 
608917     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 63.49ms 
608918     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermFromSwap.proof 
608919     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 61.2ns 
608919     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
611313     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.39s 
611313     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermFromSwap 
612102     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermFromSwap 
612132     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 26.31ms 
612134     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermTransAlt0.proof 
612134     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 49.3ns 
612134     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
614509     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.38s 
614510     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermTransAlt0 
615295     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermTransAlt0 
615297     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 240.9ns 
615298     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermTransAlt1.proof 
615298     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 43.3ns 
615299     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
617690     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.39s 
617690     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermTransAlt1 
618475     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermTransAlt1 
618476     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 200.7ns 
618478     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermTransAlt2.proof 
618478     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 53.1ns 
618478     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
620896     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.42s 
620896     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermTransAlt2 
621686     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermTransAlt2 
621687     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 191.6ns 
621689     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermTransAlt3.proof 
621689     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 48.2ns 
621689     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
624069     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.38s 
624069     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermTransAlt3 
624859     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermTransAlt3 
624861     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 323.6ns 
624862     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermForall.proof 
624862     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 53.6ns 
624862     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
627259     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.4s 
627259     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermForall 
628046     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermForall 
628140     INFO  Test worker     d.u.i.k.s.SMTFocusResults Analyzing unsat core: (L_1 L_3 L_4) 
628151     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 102.65ms 
628154     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermExists.proof 
628154     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 187.3ns 
628155     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
630552     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.4s 
630552     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermExists 
631401     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermExists 
631439     INFO  Test worker     d.u.i.k.s.SMTFocusResults Analyzing unsat core: (L_1 L_3 L_5 L_6 L_7) 
631443     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 40.43ms 
631444     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm2/Taclet_schiffl_lemma_2.proof 
631445     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 45ns 
631445     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
633878     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.43s 
633878     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: schiffl_lemma_2 
634659     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: schiffl_lemma_2 
634660     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.6ns 
634687     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [1] goal: 0, source line: 49, command: 'macro split-prop' 
634734     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [2] goal: 3, source line: 50, command: 'rule allRight' 
634753     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [3] goal: 4, source line: 51, command: 'rule allRight' 
634759     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [4] goal: 5, source line: 52, command: 'macro split-prop' 
634774     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [5] goal: 11, source line: 53, command: 'rule 'seqPermDefLeft'' 
634777     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [6] goal: 12, source line: 54, command: 'rule 'andLeft'' 
634779     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [7] goal: 13, source line: 55, command: 'rule 'exLeft'' 
634780     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [8] goal: 14, source line: 56, command: 'macro split-prop' 
634786     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [9] goal: 16, source line: 57, command: 'rule  seqNPermRange' 
634789     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' 
634791     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [11] goal: 18, source line: 60, command: 'rule impLeft' 
634795     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [12] goal: 19, source line: 61, command: 'tryclose branch' 
635021     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [13] goal: 20, source line: 62, command: 'rule andLeft' 
635022     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [14] goal: 97, source line: 63, command: 'rule andLeft' 
635025     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' 
635026     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [16] goal: 99, source line: 66, command: 'rule impLeft' 
635028     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [17] goal: 100, source line: 67, command: 'tryclose branch' 
635147     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [18] goal: 101, source line: 68, command: 'rule andLeft' 
635148     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [19] goal: 188, source line: 69, command: 'rule andLeft' 
635149     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [20] goal: 189, source line: 70, command: 'rule seqNPermDefLeft' 
635150     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' 
635151     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [22] goal: 191, source line: 73, command: 'rule impLeft' 
635152     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [23] goal: 192, source line: 74, command: 'tryclose branch' 
635300     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [24] goal: 193, source line: 75, command: 'rule exLeft' 
635301     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [25] goal: 310, source line: 76, command: 'rule andLeft' 
635302     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [26] goal: 311, source line: 77, command: 'rule andLeft' 
635303     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' 
635303     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [28] goal: 313, source line: 80, command: 'rule impLeft' 
635304     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [29] goal: 314, source line: 81, command: 'tryclose branch' 
635414     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [30] goal: 315, source line: 82, command: 'rule exLeft' 
635415     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [31] goal: 420, source line: 83, command: 'rule andLeft' 
635416     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [32] goal: 421, source line: 84, command: 'rule andLeft' 
635417     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' 
635418     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [34] goal: 423, source line: 87, command: 'rule impLeft' 
635419     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [35] goal: 424, source line: 88, command: 'tryclose branch' 
635426     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [36] goal: 425, source line: 89, command: 'rule andLeft' 
635427     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [37] goal: 434, source line: 90, command: 'rule andLeft' 
635428     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' 
635429     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' 
635430     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [40] goal: 437, source line: 94, command: 'rule impLeft' 
635431     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [41] goal: 438, source line: 95, command: 'tryclose branch' 
635437     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [42] goal: 439, source line: 96, command: 'rule andLeft' 
635437     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [43] goal: 448, source line: 97, command: 'rule andLeft' 
635440     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' 
635441     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [45] goal: 450, source line: 99, command: 'instantiate var=iv  with='v_x_0'' 
635442     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [46] goal: 451, source line: 101, command: 'rule impLeft' 
635442     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [47] goal: 452, source line: 102, command: 'tryclose branch' 
635625     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [48] goal: 453, source line: 103, command: 'instantiate var=iv  with='v_y_0'' 
635626     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [49] goal: 562, source line: 105, command: 'rule impLeft' 
635627     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [50] goal: 563, source line: 106, command: 'tryclose branch' 
635773     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [51] goal: 564, source line: 107, command: 'cut 'v_x_0 = v_y_0'' 
635774     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)'' 
635775     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [53] goal: 676, source line: 111, command: 'rule andRight' 
635777     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [54] goal: 677, source line: 113, command: 'rule andRight' 
635778     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [55] goal: 679, source line: 114, command: 'rule andRight' 
635778     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [56] goal: 681, source line: 115, command: 'rule andRight' 
635779     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [57] goal: 683, source line: 116, command: 'rule lenOfSwap' 
635780     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [58] goal: 685, source line: 117, command: 'tryclose branch' 
635784     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [59] goal: 684, source line: 118, command: 'rule seqNPermSwapNPerm' 
635785     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' 
635786     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [61] goal: 688, source line: 121, command: 'instantiate hide var='jv' with='jv_0'' 
635787     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [62] goal: 689, source line: 122, command: 'rule impLeft' 
635787     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [63] goal: 690, source line: 123, command: 'tryclose branch' 
635916     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [64] goal: 691, source line: 124, command: 'tryclose branch' 
635920     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [65] goal: 682, source line: 125, command: 'rule allRight' 
635921     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [66] goal: 796, source line: 127, command: 'rule impRight' 
635922     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [67] goal: 797, source line: 128, command: 'rule andLeft' 
635923     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [68] goal: 798, source line: 129, command: 'instantiate var=iv with='v_iv_0'' 
635923     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [69] goal: 799, source line: 130, command: 'rule impLeft' 
635924     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [70] goal: 800, source line: 131, command: 'tryclose branch' 
636065     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [71] goal: 801, source line: 132, command: 'rule getOfSwap' 
636066     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [72] goal: 912, source line: 133, command: 'rule ifthenelse_negated' 
636067     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [73] goal: 913, source line: 134, command: 'rule ifthenelse_split occ=0' 
636069     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [74] goal: 914, source line: 135, command: 'rule andLeft' 
636070     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [75] goal: 916, source line: 136, command: 'rule andLeft' 
636070     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [76] goal: 917, source line: 137, command: 'rule andLeft' 
636071     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [77] goal: 918, source line: 138, command: 'rule ifthenelse_split occ=0' 
636072     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [78] goal: 919, source line: 139, command: 'tryclose branch' 
636185     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [79] goal: 920, source line: 140, command: 'rule ifthenelse_split occ=0' 
636187     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [80] goal: 1011, source line: 141, command: 'tryclose branch' 
636276     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [81] goal: 1012, source line: 142, command: 'tryclose branch' 
636280     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [82] goal: 915, source line: 143, command: 'tryclose branch' 
636284     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [83] goal: 680, source line: 144, command: 'rule getOfSwap' 
636285     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [84] goal: 1099, source line: 146, command: 'rule ifthenelse_negated' 
636286     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [85] goal: 1100, source line: 147, command: 'rule ifthenelse_split occ=0' 
636287     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [86] goal: 1101, source line: 148, command: 'rule andLeft' 
636288     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [87] goal: 1103, source line: 149, command: 'rule andLeft' 
636289     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [88] goal: 1104, source line: 150, command: 'rule andLeft' 
636289     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [89] goal: 1105, source line: 151, command: 'rule ifthenelse_split occ=0' 
636290     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [90] goal: 1106, source line: 152, command: 'tryclose branch' 
636297     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [91] goal: 1107, source line: 153, command: 'tryclose branch' 
636301     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [92] goal: 1102, source line: 154, command: 'tryclose branch' 
636385     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [93] goal: 678, source line: 155, command: 'rule getOfSwap' 
636386     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [94] goal: 1225, source line: 157, command: 'rule ifthenelse_negated' 
636387     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [95] goal: 1226, source line: 158, command: 'rule ifthenelse_split occ=0' 
636388     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [96] goal: 1227, source line: 159, command: 'rule andLeft' 
636389     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [97] goal: 1229, source line: 160, command: 'rule andLeft' 
636390     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [98] goal: 1230, source line: 161, command: 'rule andLeft' 
636390     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [99] goal: 1231, source line: 162, command: 'rule ifthenelse_split occ=0' 
636391     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [100] goal: 1232, source line: 163, command: 'tryclose branch' 
636437     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [101] goal: 1233, source line: 164, command: 'tryclose branch' 
636442     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [102] goal: 1228, source line: 165, command: 'tryclose branch' 
636520     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]'' 
636521     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [104] goal: 1397, source line: 169, command: 'rule seqNPermInjective' 
636522     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'' 
636523     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'' 
636524     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [107] goal: 1401, source line: 172, command: 'rule impLeft' 
636525     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [108] goal: 1402, source line: 173, command: 'tryclose branch' 
636653     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [109] goal: 1403, source line: 174, command: 'tryclose branch' 
636656     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'' 
636657     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)'' 
636658     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [112] goal: 1536, source line: 179, command: 'rule andRight' 
636659     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [113] goal: 1537, source line: 181, command: 'rule andRight' 
636660     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [114] goal: 1539, source line: 182, command: 'rule andRight' 
636661     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [115] goal: 1541, source line: 183, command: 'rule andRight' 
636661     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [116] goal: 1543, source line: 184, command: 'tryclose branch' 
636669     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [117] goal: 1544, source line: 185, command: 'rule seqNPermSwapNPerm' 
636670     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'' 
636671     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [119] goal: 1559, source line: 188, command: 'instantiate hide var=jv with='jv_1'' 
636672     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [120] goal: 1560, source line: 189, command: 'tryclose branch' 
636750     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [121] goal: 1542, source line: 190, command: 'rule allRight' 
636751     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [122] goal: 1667, source line: 192, command: 'rule impRight' 
636752     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [123] goal: 1668, source line: 193, command: 'rule andLeft' 
636752     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [124] goal: 1669, source line: 194, command: 'instantiate var=iv with='v_iv_0'' 
636753     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [125] goal: 1670, source line: 195, command: 'rule impLeft' 
636754     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [126] goal: 1671, source line: 196, command: 'tryclose branch' 
636839     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [127] goal: 1672, source line: 197, command: 'rule getOfSwap' 
636840     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [128] goal: 1786, source line: 198, command: 'rule ifthenelse_negated' 
636841     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [129] goal: 1787, source line: 199, command: 'rule ifthenelse_split occ=0' 
636842     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [130] goal: 1788, source line: 200, command: 'rule andLeft' 
636843     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [131] goal: 1790, source line: 201, command: 'rule andLeft' 
636843     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [132] goal: 1791, source line: 202, command: 'rule andLeft' 
636844     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [133] goal: 1792, source line: 203, command: 'rule ifthenelse_split occ=0' 
636845     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [134] goal: 1793, source line: 204, command: 'tryclose branch' 
636915     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [135] goal: 1794, source line: 205, command: 'rule ifthenelse_split occ=0' 
636916     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [136] goal: 1885, source line: 206, command: 'tryclose branch' 
636980     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [137] goal: 1886, source line: 207, command: 'instantiate var=iv with='v_y_0'' 
636980     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [138] goal: 1968, source line: 208, command: 'rule impLeft' 
636981     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [139] goal: 1969, source line: 209, command: 'tryclose branch' 
636985     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [140] goal: 1970, source line: 210, command: 'tryclose branch' 
636988     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [141] goal: 1789, source line: 211, command: 'tryclose branch' 
636992     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [142] goal: 1540, source line: 212, command: 'tryclose branch' 
637094     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [143] goal: 1538, source line: 213, command: 'rule getOfSwap' 
637095     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [144] goal: 2097, source line: 215, command: 'rule ifthenelse_negated' 
637096     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [145] goal: 2098, source line: 216, command: 'rule ifthenelse_split occ=0' 
637097     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [146] goal: 2099, source line: 217, command: 'tryclose branch' 
637105     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [147] goal: 2100, source line: 218, command: 'tryclose branch' 
637178     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [148] goal: 1535, source line: 219, command: 'tryclose branch' 
640314     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'' 
640315     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)'' 
640319     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [151] goal: 4268, source line: 226, command: 'rule andRight' 
640321     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [152] goal: 4269, source line: 228, command: 'rule andRight' 
640322     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [153] goal: 4271, source line: 229, command: 'rule andRight' 
640323     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [154] goal: 4273, source line: 230, command: 'rule andRight' 
640323     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [155] goal: 4275, source line: 231, command: 'tryclose branch' 
640331     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [156] goal: 4276, source line: 232, command: 'rule seqNPermSwapNPerm' 
640331     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'' 
640332     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [158] goal: 4288, source line: 235, command: 'instantiate hide var=jv with='jv_0'' 
640333     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [159] goal: 4289, source line: 236, command: 'rule impLeft' 
640334     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [160] goal: 4290, source line: 237, command: 'tryclose branch' 
640419     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [161] goal: 4291, source line: 238, command: 'tryclose branch' 
640423     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [162] goal: 4274, source line: 239, command: 'rule allRight' 
640423     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [163] goal: 4400, source line: 241, command: 'rule impRight' 
640424     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [164] goal: 4401, source line: 242, command: 'rule andLeft' 
640425     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [165] goal: 4402, source line: 243, command: 'instantiate var=iv with='v_iv_0'' 
640425     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [166] goal: 4403, source line: 244, command: 'rule impLeft' 
640426     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [167] goal: 4404, source line: 245, command: 'tryclose branch' 
640510     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [168] goal: 4405, source line: 246, command: 'rule getOfSwap' 
640511     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [169] goal: 4521, source line: 247, command: 'rule ifthenelse_negated' 
640512     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [170] goal: 4522, source line: 248, command: 'rule ifthenelse_split occ=0' 
640513     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [171] goal: 4523, source line: 249, command: 'rule andLeft' 
640514     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [172] goal: 4525, source line: 250, command: 'rule andLeft' 
640515     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [173] goal: 4526, source line: 251, command: 'rule andLeft' 
640515     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [174] goal: 4527, source line: 252, command: 'rule ifthenelse_split occ=0' 
640516     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [175] goal: 4528, source line: 253, command: 'tryclose branch' 
640584     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [176] goal: 4529, source line: 254, command: 'rule ifthenelse_split occ=0' 
640585     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [177] goal: 4622, source line: 255, command: 'tryclose branch' 
640653     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [178] goal: 4623, source line: 256, command: 'tryclose branch' 
640657     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [179] goal: 4524, source line: 257, command: 'tryclose branch' 
640662     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [180] goal: 4272, source line: 258, command: 'rule getOfSwap' 
640662     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [181] goal: 4713, source line: 260, command: 'rule ifthenelse_negated' 
640663     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [182] goal: 4714, source line: 261, command: 'rule ifthenelse_split occ=0' 
640664     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [183] goal: 4715, source line: 262, command: 'tryclose branch' 
640673     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [184] goal: 4716, source line: 263, command: 'tryclose branch' 
640746     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [185] goal: 4270, source line: 264, command: 'rule getOfSwap' 
640747     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [186] goal: 4839, source line: 266, command: 'rule ifthenelse_negated' 
640747     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [187] goal: 4840, source line: 267, command: 'rule ifthenelse_split occ=0' 
640748     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [188] goal: 4841, source line: 268, command: 'tryclose branch' 
640814     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [189] goal: 4842, source line: 269, command: 'tryclose branch' 
640822     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'' 
640823     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)'' 
640823     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [192] goal: 4950, source line: 275, command: 'rule andRight' 
640825     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [193] goal: 4951, source line: 277, command: 'rule andRight' 
640825     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [194] goal: 4953, source line: 278, command: 'rule andRight' 
640825     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [195] goal: 4955, source line: 279, command: 'rule andRight' 
640826     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [196] goal: 4957, source line: 280, command: 'tryclose branch' 
640835     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [197] goal: 4958, source line: 281, command: 'rule seqNPermSwapNPerm' 
640836     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [198] goal: 4977, source line: 283, command: 'instantiate hide var=iv with='jv_0'' 
640837     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'' 
640837     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [200] goal: 4979, source line: 285, command: 'rule impLeft' 
640838     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [201] goal: 4980, source line: 286, command: 'tryclose branch' 
640917     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))'' 
640917     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [203] goal: 5093, source line: 288, command: 'instantiate hide var=iv with='jv_0'' 
640918     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'' 
640919     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [205] goal: 5095, source line: 290, command: 'rule impLeft' 
640920     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [206] goal: 5096, source line: 291, command: 'tryclose branch' 
641001     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [207] goal: 5097, source line: 292, command: 'tryclose branch' 
641005     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [208] goal: 4956, source line: 293, command: 'rule allRight' 
641006     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [209] goal: 5212, source line: 295, command: 'rule impRight' 
641007     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [210] goal: 5213, source line: 296, command: 'rule andLeft' 
641007     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [211] goal: 5214, source line: 297, command: 'instantiate var=iv with='v_iv_0'' 
641007     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [212] goal: 5215, source line: 300, command: 'rule impLeft' 
641008     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [213] goal: 5216, source line: 301, command: 'tryclose branch' 
641096     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [214] goal: 5217, source line: 302, command: 'rule getOfSwap' 
641097     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [215] goal: 5337, source line: 304, command: 'rule ifthenelse_negated' 
641098     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [216] goal: 5338, source line: 305, command: 'rule ifthenelse_split occ=0' 
641099     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [217] goal: 5339, source line: 306, command: 'rule andLeft' 
641099     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [218] goal: 5341, source line: 307, command: 'rule andLeft' 
641100     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [219] goal: 5342, source line: 308, command: 'rule andLeft' 
641100     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [220] goal: 5343, source line: 309, command: 'rule ifthenelse_split occ=0' 
641101     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [221] goal: 5344, source line: 310, command: 'rule getOfSwap' 
641101     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [222] goal: 5346, source line: 311, command: 'rule ifthenelse_negated' 
641102     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [223] goal: 5347, source line: 312, command: 'rule ifthenelse_split occ=0' 
641103     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [224] goal: 5348, source line: 313, command: 'rule andLeft' 
641103     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [225] goal: 5350, source line: 314, command: 'rule andLeft' 
641104     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [226] goal: 5351, source line: 315, command: 'rule andLeft' 
641104     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [227] goal: 5352, source line: 316, command: 'rule ifthenelse_split occ=0' 
641104     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [228] goal: 5353, source line: 317, command: 'tryclose branch' 
641185     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [229] goal: 5354, source line: 318, command: 'rule ifthenelse_split occ=0' 
641186     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [230] goal: 5463, source line: 319, command: 'tryclose branch' 
641192     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [231] goal: 5464, source line: 320, command: 'tryclose branch' 
641263     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [232] goal: 5349, source line: 321, command: 'tryclose branch' 
641335     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [233] goal: 5345, source line: 322, command: 'rule ifthenelse_split' 
641336     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [234] goal: 5660, source line: 324, command: 'rule getOfSwap' 
641337     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [235] goal: 5662, source line: 325, command: 'rule ifthenelse_negated' 
641337     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [236] goal: 5663, source line: 326, command: 'rule ifthenelse_split occ=0' 
641338     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [237] goal: 5664, source line: 327, command: 'rule andLeft' 
641339     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [238] goal: 5666, source line: 328, command: 'rule andLeft' 
641339     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [239] goal: 5667, source line: 329, command: 'rule andLeft' 
641339     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [240] goal: 5668, source line: 330, command: 'rule ifthenelse_split occ=0' 
641340     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [241] goal: 5669, source line: 331, command: 'tryclose branch' 
641418     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [242] goal: 5670, source line: 332, command: 'tryclose branch' 
641424     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [243] goal: 5665, source line: 333, command: 'tryclose branch' 
641506     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [244] goal: 5661, source line: 334, command: 'rule getOfSwap' 
641507     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [245] goal: 5887, source line: 336, command: 'rule ifthenelse_negated' 
641507     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [246] goal: 5888, source line: 337, command: 'rule ifthenelse_split occ=0' 
641508     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [247] goal: 5889, source line: 338, command: 'rule andLeft' 
641509     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [248] goal: 5891, source line: 339, command: 'rule andLeft' 
641509     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [249] goal: 5892, source line: 340, command: 'rule andLeft' 
641509     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [250] goal: 5893, source line: 341, command: 'rule ifthenelse_split occ=0' 
641510     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [251] goal: 5894, source line: 342, command: 'tryclose branch' 
641515     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [252] goal: 5895, source line: 343, command: 'rule ifthenelse_split occ=0' 
641515     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [253] goal: 5897, source line: 344, command: 'tryclose branch' 
641588     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [254] goal: 5898, source line: 345, command: 'tryclose branch' 
641593     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [255] goal: 5890, source line: 346, command: 'tryclose branch' 
641598     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [256] goal: 5340, source line: 347, command: 'tryclose branch' 
641724     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [257] goal: 4954, source line: 348, command: 'rule getOfSwap' 
641724     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [258] goal: 6115, source line: 350, command: 'rule ifthenelse_negated' 
641725     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [259] goal: 6116, source line: 351, command: 'rule ifthenelse_split occ=0' 
641726     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [260] goal: 6117, source line: 352, command: 'rule andLeft' 
641726     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [261] goal: 6119, source line: 353, command: 'rule andLeft' 
641727     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [262] goal: 6120, source line: 354, command: 'rule andLeft' 
641727     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [263] goal: 6121, source line: 355, command: 'rule ifthenelse_split occ=0' 
641727     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [264] goal: 6122, source line: 356, command: 'tryclose branch' 
641776     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [265] goal: 6123, source line: 357, command: 'rule ifthenelse_split occ=0' 
641776     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [266] goal: 6193, source line: 358, command: 'rule getOfSwap' 
641777     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [267] goal: 6195, source line: 359, command: 'rule ifthenelse_negated' 
641777     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [268] goal: 6196, source line: 360, command: 'rule ifthenelse_split occ=0' 
641778     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [269] goal: 6197, source line: 361, command: 'tryclose branch' 
641783     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [270] goal: 6198, source line: 362, command: 'tryclose branch' 
641787     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [271] goal: 6194, source line: 363, command: 'tryclose branch' 
641891     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [272] goal: 6118, source line: 364, command: 'tryclose branch' 
641969     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [273] goal: 4952, source line: 365, command: 'rule getOfSwap' 
641970     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [274] goal: 6456, source line: 367, command: 'rule ifthenelse_negated' 
641971     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [275] goal: 6457, source line: 368, command: 'rule ifthenelse_split occ=0' 
641971     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [276] goal: 6458, source line: 369, command: 'tryclose branch' 
642122     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [277] goal: 6459, source line: 370, command: 'tryclose branch' 
642201     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'' 
642201     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [279] goal: 6735, source line: 375, command: 'tryclose branch' 
644901     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [280] goal: 6735, source line: 378, command: 'rule seqNPermSwapNPerm' 
644906     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [281] goal: 8783, source line: 380, command: 'instantiate hide var=iv with='jv_1'' 
644907     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'' 
644908     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [283] goal: 8785, source line: 382, command: 'rule impLeft' 
644908     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [284] goal: 8786, source line: 383, command: 'tryclose branch' 
645011     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))'' 
645012     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [286] goal: 8909, source line: 385, command: 'instantiate hide var=iv with='jv_1'' 
645013     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'' 
645013     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [288] goal: 8911, source line: 387, command: 'rule impLeft' 
645014     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [289] goal: 8912, source line: 388, command: 'tryclose branch' 
645108     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [290] goal: 8913, source line: 389, command: 'tryclose branch' 
647751     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [291] goal: 6736, source line: 390, command: 'tryclose branch' 
650619     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [292] goal: 6736, source line: 397, command: 'rule seqNPermSwapNPerm formula='seqNPerm(s_0)'' 
650623     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'' 
650624     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [294] goal: 12634, source line: 400, command: 'instantiate hide var=jv with='jv_0'' 
650625     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [295] goal: 12635, source line: 401, command: 'rule impLeft' 
650626     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [296] goal: 12636, source line: 402, command: 'tryclose branch' 
650727     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))'' 
650727     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'' 
650728     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [299] goal: 12758, source line: 405, command: 'instantiate hide var=jv with='jv_1'' 
650729     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)' ...' 
650730     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [301] goal: 12760, source line: 407, command: 'tryclose branch' 
651707     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm2/Taclet_schiffl_thm_1.proof 
651708     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 73ns 
651708     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
654207     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.5s 
654208     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: schiffl_thm_1 
655025     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: schiffl_thm_1 
655026     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 7.7ns 
655027     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [1] goal: 0, source line: 50, command: 'macro split-prop' 
655035     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)'' 
655044     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [3] goal: 11, source line: 52, command: 'instantiate hide var=x with='f_x'' 
655046     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [4] goal: 12, source line: 53, command: 'instantiate hide var=y with='f_y'' 
655048     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [5] goal: 13, source line: 54, command: 'rule impLeft' 
655050     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [6] goal: 14, source line: 55, command: 'tryclose branch' 
655054     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [7] goal: 15, source line: 56, command: 'rule exLeft' 
655054     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [8] goal: 23, source line: 57, command: 'macro split-prop' 
655059     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [9] goal: 27, source line: 58, command: 'rule seqPermDef occ=1' 
655059     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [10] goal: 28, source line: 59, command: 'rule andRight' 
655061     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [11] goal: 29, source line: 60, command: 'tryclose branch' 
655071     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [12] goal: 30, source line: 61, command: 'instantiate hide var=s with='r_0'' 
655071     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [13] goal: 46, source line: 62, command: 'rule andRight' 
655073     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [14] goal: 47, source line: 63, command: 'tryclose branch' 
655122     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [15] goal: 48, source line: 64, command: 'rule allRight' 
655123     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [16] goal: 119, source line: 65, command: 'rule impRight' 
655123     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [17] goal: 120, source line: 66, command: 'instantiate hide var=iv with='iv_0'' 
655124     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [18] goal: 121, source line: 67, command: 'rule impLeft' 
655124     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [19] goal: 122, source line: 68, command: 'tryclose branch' 
655190     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [20] goal: 123, source line: 69, command: 'rule andLeft' 
655191     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [21] goal: 203, source line: 70, command: 'rule seqNPermRange' 
655191     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [22] goal: 204, source line: 71, command: 'instantiate hide var=iv with='iv_0'' 
655192     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [23] goal: 205, source line: 72, command: 'rule impLeft' 
655192     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [24] goal: 206, source line: 73, command: 'tryclose branch' 
655196     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [25] goal: 207, source line: 74, command: 'rule andLeft' 
655197     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [26] goal: 215, source line: 75, command: 'rule andLeft' 
655197     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [27] goal: 216, source line: 76, command: 'rule seqNPermRange' 
655197     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [28] goal: 217, source line: 77, command: 'instantiate hide var=iv with='f_x'' 
655198     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [29] goal: 218, source line: 78, command: 'rule impLeft' 
655199     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [30] goal: 219, source line: 79, command: 'tryclose branch' 
655281     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [31] goal: 220, source line: 80, command: 'rule andLeft' 
655281     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [32] goal: 311, source line: 81, command: 'rule andLeft' 
655282     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [33] goal: 312, source line: 82, command: 'rule seqNPermRange' 
655283     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [34] goal: 313, source line: 83, command: 'instantiate hide var=iv with='f_y'' 
655284     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [35] goal: 314, source line: 84, command: 'rule impLeft' 
655284     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [36] goal: 315, source line: 85, command: 'tryclose branch' 
655366     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [37] goal: 316, source line: 86, command: 'rule andLeft' 
655366     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [38] goal: 410, source line: 87, command: 'rule andLeft' 
655367     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [39] goal: 411, source line: 88, command: 'rule getOfSeqDef occ=0' 
655368     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [40] goal: 412, source line: 89, command: 'rule getOfSeqDef' 
655368     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [41] goal: 413, source line: 90, command: 'rule ifthenelse_split occ=0' 
655369     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [42] goal: 414, source line: 91, command: 'rule andLeft occ=0' 
655370     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [43] goal: 416, source line: 92, command: 'rule sub_zero_2 occ=0' 
655370     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [44] goal: 417, source line: 93, command: 'rule ifthenelse_split occ=2' 
655371     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [45] goal: 418, source line: 94, command: 'rule andLeft' 
655371     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [46] goal: 420, source line: 95, command: 'rule sub_zero_2 occ=0' 
655372     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [47] goal: 421, source line: 96, command: 'rule add_zero_right occ=0' 
655372     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [48] goal: 422, source line: 97, command: 'rule add_zero_right occ=0' 
655372     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [49] goal: 423, source line: 98, command: 'rule add_zero_right occ=0' 
655373     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [50] goal: 424, source line: 99, command: 'rule add_zero_right occ=0' 
655373     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [51] goal: 425, source line: 100, command: 'rule add_zero_right occ=0' 
655374     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [52] goal: 426, source line: 101, command: 'rule add_zero_right occ=0' 
655374     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [53] goal: 427, source line: 102, command: 'rule ifthenelse_split occ=0' 
655375     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [54] goal: 428, source line: 103, command: 'rule ifthenelse_split occ=0' 
655376     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [55] goal: 430, source line: 104, command: 'tryclose branch' 
655378     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [56] goal: 431, source line: 105, command: 'tryclose branch' 
655414     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [57] goal: 429, source line: 106, command: 'rule ifthenelse_split occ=0' 
655415     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [58] goal: 473, source line: 107, command: 'tryclose branch' 
655473     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [59] goal: 474, source line: 108, command: 'rule ifthenelse_split occ=0' 
655474     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [60] goal: 541, source line: 109, command: 'rule seqNPermInjective' 
655475     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [61] goal: 543, source line: 110, command: 'instantiate hide var=iv with='iv_0'' 
655476     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [62] goal: 544, source line: 111, command: 'instantiate hide var=jv with='f_y'' 
655477     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [63] goal: 545, source line: 112, command: 'rule impLeft' 
655478     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [64] goal: 546, source line: 113, command: 'tryclose branch' 
655521     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [65] goal: 547, source line: 114, command: 'tryclose branch' 
655523     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [66] goal: 542, source line: 115, command: 'rule ifthenelse_split occ=0' 
655524     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [67] goal: 606, source line: 116, command: 'rule seqNPermInjective' 
655525     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [68] goal: 608, source line: 117, command: 'instantiate hide var=iv with='iv_0'' 
655526     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [69] goal: 609, source line: 118, command: 'instantiate hide var=jv with='f_x'' 
655527     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [70] goal: 610, source line: 119, command: 'rule impLeft' 
655528     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [71] goal: 611, source line: 120, command: 'tryclose branch' 
655571     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [72] goal: 612, source line: 121, command: 'tryclose branch' 
655573     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [73] goal: 607, source line: 122, command: 'tryclose branch' 
655576     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [74] goal: 419, source line: 123, command: 'tryclose branch' 
655620     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [75] goal: 415, source line: 124, command: 'tryclose branch' 
655668     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_eqSameSeq.proof 
655668     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 203.1ns 
655669     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
658170     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.5s 
658170     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: eqSameSeq 
659005     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: eqSameSeq 
659019     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 11.74ms