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

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

tests
0

failures
0

ignored
14m9.40s

duration
100%

successful

Tests

Test Method name Duration Result
powPositive data()[100] 4.207s passed
powPositiveConcrete data()[101] 4.231s passed
powGeq1Concrete data()[102] 4.236s passed
pow2InIntLower data()[103] 4.191s passed
pow2InIntUpper data()[104] 4.208s passed
logSelfConcrete data()[105] 4.261s passed
log1Concrete data()[106] 4.235s passed
logProduct data()[107] 4.224s passed
logTimesBaseConcrete data()[108] 4.324s passed
logProdIdentity data()[109] 4.246s passed
moduloByteIsInByte data()[10] 4.222s passed
logProdIdentityConcrete data()[110] 4.116s passed
logPowIdentity data()[111] 4.032s passed
logPowIdentityConcrete data()[112] 4.021s passed
logPositive data()[113] 4.070s passed
logPositiveConcrete data()[114] 4.046s passed
logMono data()[115] 4.003s passed
logMonoConcrete data()[116] 4.083s passed
powLogLess data()[117] 4.115s passed
powLogMore2 data()[118] 4.116s passed
logLessThanPow data()[119] 4.136s passed
moduloCharIsInChar data()[11] 4.150s passed
logLessThanPowConcrete data()[120] 4.210s passed
logSqueeze data()[121] 4.255s passed
ifthenelse_equals data()[122] 4.166s passed
ifthenelse_equals_1 data()[123] 4.310s passed
ifthenelse_equals_2 data()[124] 4.161s passed
disjointWithSingleton1 data()[125] 4.221s passed
disjointWithSingleton2 data()[126] 4.074s passed
disjointArrayRanges data()[127] 4.130s passed
disjointArrayRangeAllFields1 data()[128] 4.143s passed
disjointArrayRangeAllFields2 data()[129] 4.273s passed
div_unique1 data()[12] 4.226s passed
seqSelfDefinition data()[130] 4.405s passed
seqOutsideValue data()[131] 4.281s passed
castedGetAny data()[132] 4.295s passed
seqGetAlphaCast data()[133] 4.246s passed
getOfSeqSingleton data()[134] 4.277s passed
getOfSeqSingletonConcrete data()[135] 4.246s passed
getOfSeqConcat data()[136] 4.326s passed
getOfSeqSub data()[137] 4.227s passed
getOfSeqReverse data()[138] 4.287s passed
lenOfSeqEmpty data()[139] 4.339s passed
div_unique2 data()[13] 4.204s passed
lenOfSeqSingleton data()[140] 4.246s passed
lenOfSeqConcat data()[141] 4.225s passed
lenOfSeqSub data()[142] 4.054s passed
lenOfSeqReverse data()[143] 4.054s passed
equalityToSeqGetAndSeqLenLeft data()[144] 3.994s passed
equalityToSeqGetAndSeqLenRight data()[145] 4.077s passed
getOfSeqSingletonEQ data()[146] 3.980s passed
getOfSeqConcatEQ data()[147] 4.039s passed
getOfSeqSubEQ data()[148] 4.018s passed
getOfSeqReverseEQ data()[149] 3.992s passed
div_exists data()[14] 4.409s passed
lenOfSeqEmptyEQ data()[150] 4.107s passed
lenOfSeqSingletonEQ data()[151] 3.985s passed
lenOfSeqConcatEQ data()[152] 4.085s passed
lenOfSeqSubEQ data()[153] 4.080s passed
lenOfSeqReverseEQ data()[154] 4.041s passed
getOfSeqDefEQ data()[155] 4.039s passed
lenOfSeqDefEQ data()[156] 4.045s passed
seqConcatWithSeqEmpty1 data()[157] 4.111s passed
seqConcatWithSeqEmpty2 data()[158] 4.031s passed
seqReverseOfSeqEmpty data()[159] 4.034s passed
div_one data()[15] 4.118s passed
subSeqComplete data()[160] 4.091s passed
subSeqTailR data()[161] 3.983s passed
subSeqTailL data()[162] 4.046s passed
subSeqTailEQR data()[163] 4.293s passed
subSeqTailEQL data()[164] 4.235s passed
seqDef_split data()[165] 4.333s passed
seqDef_induction_upper data()[166] 4.447s passed
seqDef_induction_upper_concrete data()[167] 4.370s passed
seqDef_induction_lower data()[168] 4.434s passed
seqDef_induction_lower_concrete data()[169] 4.301s passed
jdiv_one data()[16] 4.192s passed
seqDef_split_in_three data()[170] 4.354s passed
seqDef_empty data()[171] 4.272s passed
seqDef_one_summand data()[172] 4.276s passed
seqDef_lower_equals_upper data()[173] 4.235s passed
seqDefOfSeq data()[174] 4.226s passed
seqSelfDefinitionEQ2 data()[175] 4.221s passed
indexOfSeqSingleton data()[176] 4.243s passed
indexOfSeqConcatFirst data()[177] 4.233s passed
indexOfSeqConcatSecond data()[178] 4.191s passed
indexOfSeqSub data()[179] 4.232s passed
div_zero data()[17] 4.186s passed
lenOfArray2seq data()[180] 4.211s passed
getAnyOfArray2seq data()[181] 4.239s passed
getOfArray2seq data()[182] 4.489s passed
getAnyOfNPermInv data()[183] 4.276s passed
seqNPermRange data()[184] 4.135s passed
seqPermTrans data()[185] 4.127s passed
seqPermRefl data()[186] 4.035s passed
seqPermSplit data()[187] 3.927s passed
seqNPermRight data()[188] 4.092s passed
seqPermFromSwap data()[189] 4.061s passed
divResZero1 data()[18] 4.203s passed
seqPermTransAlt0 data()[190] 4.137s passed
seqPermTransAlt1 data()[191] 4.130s passed
seqPermTransAlt2 data()[192] 4.113s passed
seqPermTransAlt3 data()[193] 4.025s passed
seqPermForall data()[194] 4.181s passed
seqPermExists data()[195] 4.172s passed
schiffl_lemma_2 data()[196] 28.114s passed
schiffl_thm_1 data()[197] 5.338s passed
eqSameSeq data()[198] 4.256s passed
divResZero2 data()[19] 4.159s passed
eqTermCut data()[1] 4.857s passed
divResOne1 data()[20] 4.241s passed
divResOne2 data()[21] 4.130s passed
div_cancel1 data()[22] 4.156s passed
div_cancel2 data()[23] 4.117s passed
divAddMultDenom data()[24] 4.151s passed
divMinus data()[25] 4.207s passed
divMinusDenom data()[26] 4.164s passed
divLeastDPos data()[27] 4.034s passed
divLeastDNeg data()[28] 4.089s passed
divGreatestDPos data()[29] 4.222s passed
equivAllRight data()[2] 4.567s passed
divGreatestDNeg data()[30] 4.021s passed
divIncreasingPos data()[31] 4.058s passed
divIncreasingNeg data()[32] 4.121s passed
jdiv_zero data()[33] 4.043s passed
jdivPulloutMinusNum data()[34] 4.058s passed
jdivPulloutMinusDenom data()[35] 4.162s passed
jdiv_uniquePosPos data()[36] 4.101s passed
jdiv_uniquePosNeg data()[37] 4.051s passed
jdiv_uniqueNegPos data()[38] 4.043s passed
jdiv_uniqueNegNeg data()[39] 4.037s passed
irrflConcrete1 data()[3] 4.423s passed
jdivMultDenom1 data()[40] 4.130s passed
jdivMultDenom2 data()[41] 4.009s passed
mod_geZero data()[42] 4.002s passed
mod_lessDenom data()[43] 4.072s passed
jmod_NumPos data()[44] 4.088s passed
jmod_NumNeg data()[45] 4.053s passed
jmod_geZero data()[46] 4.050s passed
jmodNumZero data()[47] 4.032s passed
jmod_pulloutminusNum data()[48] 4.060s passed
jmod_pulloutminusDenom data()[49] 4.037s passed
irrflConcrete2 data()[4] 4.244s passed
jmodUnique1 data()[50] 4.135s passed
jmodUnique2 data()[51] 4.140s passed
intDivRem data()[52] 3.990s passed
jmodjmod data()[53] 4.074s passed
jmodDivisible data()[54] 4.012s passed
jmodDivisibleRep data()[55] 4.015s passed
jdivAddMultDenom data()[56] 4.181s passed
jmodAltZero data()[57] 3.997s passed
jmodAddMultDenomZero data()[58] 4.041s passed
polyDiv_zero data()[59] 4.031s passed
cancel_gtPos data()[5] 4.371s passed
polyMod_ltdivDenom data()[60] 4.003s passed
bsum_empty data()[61] 3.958s passed
bsum_induction_upper data()[62] 3.995s passed
bsum_induction_lower data()[63] 4.036s passed
bsum_num_of_bounds data()[64] 4.023s passed
bsum_num_of_bounds2 data()[65] 4.048s passed
bsum_induction_upper2 data()[66] 4.120s passed
bsum_induction_upper_concrete data()[67] 3.986s passed
bsum_induction_upper_concrete_2 data()[68] 4.037s passed
bsum_induction_upper2_concrete data()[69] 4.023s passed
cancel_gtNeg data()[6] 4.264s passed
bsum_induction_lower_concrete data()[70] 3.981s passed
bsum_induction_lower2 data()[71] 4.021s passed
bsum_induction_lower2_concrete data()[72] 3.998s passed
bsum_positive data()[73] 4.146s passed
bsum_upper_bound data()[74] 4.078s passed
bsum_lower_bound data()[75] 4.121s passed
bsum_positive_lower_bound_element data()[76] 4.218s passed
bsum_sub_same_index data()[77] 4.267s passed
bsum_less_same_index data()[78] 4.272s passed
bsum_equal_except_one_index data()[79] 4.083s passed
moduloIntIsInInt data()[7] 4.258s passed
bsum_num_of_is_max data()[80] 4.239s passed
bsum_num_of_is_max2 data()[81] 4.159s passed
bsum_num_of_is_max3 data()[82] 4.233s passed
bsum_num_of_is_max4 data()[83] 4.258s passed
bsum_num_of_lt_max data()[84] 4.223s passed
bsum_num_of_lt_max2 data()[85] 4.242s passed
bsum_num_of_lt_max3 data()[86] 4.266s passed
bsum_num_of_lt_max4 data()[87] 4.209s passed
bsum_num_of_gt0 data()[88] 4.273s passed
bsum_num_of_gt0_alt data()[89] 4.253s passed
moduloLongIsInLong data()[8] 4.268s passed
bsum_add_concrete data()[90] 4.218s passed
bprod_all_positive data()[91] 4.266s passed
bprod_split data()[92] 4.224s passed
powConcrete0 data()[93] 4.251s passed
powConcrete1 data()[94] 4.209s passed
powSplitFactor data()[95] 4.242s passed
powAdd data()[96] 4.295s passed
powMono data()[97] 4.205s passed
powMonoConcrete data()[98] 4.304s passed
powMonoConcreteRight data()[99] 4.215s passed
moduloShortIsInShort data()[9] 4.241s passed

Standard output

826        INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src/test/resources/testcase/dummyTrue.key 
857        DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 11.55ms 
1156       INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
1172       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)

2265       DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for Meta 
2270       DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for Meta 
2275       DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for Meta 
2276       DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for Meta 
4328       DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for JavaBigintExpression 
10823      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 9.67s 
10916      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof dummyTrue.key 
10972      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 40.1ns 
10990      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/firstOrder/Taclet_eqTermCut.proof 
10991      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 1.73ms 
11009      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
14563      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.55s 
14566      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: eqTermCut 
15796      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: eqTermCut 
15834      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 24.96ms 
15855      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/firstOrder/Taclet_equivAllRight.proof 
15855      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 512.5ns 
15859      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
19279      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.42s 
19280      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: equivAllRight 
20400      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: equivAllRight 
20416      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 11.42ms 
20419      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_irrflConcrete1.proof 
20419      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 141.9ns 
20421      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
23735      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.31s 
23735      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: irrflConcrete1 
24832      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: irrflConcrete1 
24840      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.41ms 
24843      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_irrflConcrete2.proof 
24843      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 404.1ns 
24845      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
28012      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.17s 
28013      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: irrflConcrete2 
29071      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: irrflConcrete2 
29084      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 8.26ms 
29089      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_cancel_gtPos.proof 
29090      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 887.11ns 
29092      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
32316      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.22s 
32317      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: cancel_gtPos 
33381      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: cancel_gtPos 
33455      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 69.97ms 
33465      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_cancel_gtNeg.proof 
33466      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 668.1ns 
33467      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
36672      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.2s 
36672      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: cancel_gtNeg 
37693      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: cancel_gtNeg 
37725      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 26.35ms 
37729      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intRulesIgnoringOF/Taclet_moduloIntIsInInt.proof 
37729      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 375.2ns 
37731      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
40949      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.22s 
40950      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: moduloIntIsInInt 
41980      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: moduloIntIsInInt 
41984      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 724.6ns 
41988      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intRulesIgnoringOF/Taclet_moduloLongIsInLong.proof 
41988      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 447.7ns 
41989      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
45229      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.24s 
45230      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: moduloLongIsInLong 
46249      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: moduloLongIsInLong 
46253      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 752.8ns 
46256      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intRulesIgnoringOF/Taclet_moduloShortIsInShort.proof 
46256      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 402ns 
46258      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
49476      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.22s 
49477      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: moduloShortIsInShort 
50492      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: moduloShortIsInShort 
50495      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 767.21ns 
50498      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intRulesIgnoringOF/Taclet_moduloByteIsInByte.proof 
50499      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 558.9ns 
50500      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
53698      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.2s 
53698      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: moduloByteIsInByte 
54713      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: moduloByteIsInByte 
54717      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 853.21ns 
54720      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intRulesIgnoringOF/Taclet_moduloCharIsInChar.proof 
54720      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 380.9ns 
54722      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
57847      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.13s 
57848      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: moduloCharIsInChar 
58863      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: moduloCharIsInChar 
58867      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 780ns 
58870      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_div_unique1.proof 
58870      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 422.8ns 
58872      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
62005      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.13s 
62006      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: div_unique1 
63042      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: div_unique1 
63092      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 44.86ms 
63103      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_div_unique2.proof 
63104      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 1.69ms 
63106      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
66217      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.11s 
66217      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: div_unique2 
67252      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: div_unique2 
67299      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 42.09ms 
67304      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_div_exists.proof 
67304      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 584ns 
67306      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
70396      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.09s 
70397      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: div_exists 
71423      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: div_exists 
71709      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 273.83ms 
71714      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_div_one.proof 
71714      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 383.7ns 
71716      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
74813      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.1s 
74814      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: div_one 
75823      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: div_one 
75829      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.83ms 
75831      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdiv_one.proof 
75831      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 127.6ns 
75833      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
78959      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.13s 
78961      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdiv_one 
80012      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdiv_one 
80020      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.52ms 
80023      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_div_zero.proof 
80024      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 487.2ns 
80025      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
83099      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.07s 
83099      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: div_zero 
84121      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: div_zero 
84206      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 78.25ms 
84211      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divResZero1.proof 
84211      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 138.6ns 
84212      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
87368      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.16s 
87369      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divResZero1 
88390      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divResZero1 
88412      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 18.23ms 
88415      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divResZero2.proof 
88415      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 416.3ns 
88416      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
91544      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.13s 
91545      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divResZero2 
92527      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divResZero2 
92571      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 33.45ms 
92585      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divResOne1.proof 
92586      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 1.29ms 
92592      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
95772      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.18s 
95772      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divResOne1 
96801      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divResOne1 
96822      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 16.21ms 
96824      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divResOne2.proof 
96824      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 131.7ns 
96826      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
99932      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.11s 
99932      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divResOne2 
100933     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divResOne2 
100952     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 14.87ms 
100959     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_div_cancel1.proof 
100961     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 2.35ms 
100963     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
104078     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.11s 
104078     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: div_cancel1 
105084     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: div_cancel1 
105112     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 23.25ms 
105115     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_div_cancel2.proof 
105115     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 410.9ns 
105117     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
108211     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.09s 
108212     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: div_cancel2 
109225     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: div_cancel2 
109229     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.8ms 
109231     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divAddMultDenom.proof 
109231     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 228ns 
109232     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
112356     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.12s 
112358     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divAddMultDenom 
113326     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divAddMultDenom 
113379     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 46.24ms 
113382     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divMinus.proof 
113383     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 326.4ns 
113384     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
116501     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.12s 
116502     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divMinus 
117507     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divMinus 
117586     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 70.62ms 
117589     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divMinusDenom.proof 
117590     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 388ns 
117591     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
120681     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.09s 
120681     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divMinusDenom 
121698     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divMinusDenom 
121752     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 47.93ms 
121754     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divLeastDPos.proof 
121754     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 113.6ns 
121755     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
124783     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.03s 
124783     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divLeastDPos 
125777     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divLeastDPos 
125787     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 7.12ms 
125788     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divLeastDNeg.proof 
125788     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 101.1ns 
125789     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
128852     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.06s 
128853     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divLeastDNeg 
129857     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divLeastDNeg 
129875     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 15.02ms 
129877     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divGreatestDPos.proof 
129877     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 110.6ns 
129878     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
133128     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.25s 
133128     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divGreatestDPos 
134080     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divGreatestDPos 
134096     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 12.49ms 
134099     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divGreatestDNeg.proof 
134099     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 99.1ns 
134100     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
137123     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.02s 
137124     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divGreatestDNeg 
138108     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divGreatestDNeg 
138119     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 7.11ms 
138121     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divIncreasingPos.proof 
138121     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 269.2ns 
138122     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
141167     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.05s 
141168     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divIncreasingPos 
142159     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divIncreasingPos 
142176     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 8.14ms 
142179     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divIncreasingNeg.proof 
142179     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 324.8ns 
142180     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
145301     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.12s 
145301     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divIncreasingNeg 
146288     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divIncreasingNeg 
146297     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 6.5ms 
146299     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdiv_zero.proof 
146299     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 101.7ns 
146300     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
149361     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.06s 
149361     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdiv_zero 
150336     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdiv_zero 
150340     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.84ms 
150341     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdivPulloutMinusNum.proof 
150342     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 109.4ns 
150343     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
153401     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.06s 
153401     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdivPulloutMinusNum 
154382     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdivPulloutMinusNum 
154398     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 10.93ms 
154400     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdivPulloutMinusDenom.proof 
154401     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 326.6ns 
154404     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
157483     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.08s 
157485     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdivPulloutMinusDenom 
158487     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdivPulloutMinusDenom 
158556     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 56.8ms 
158564     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdiv_uniquePosPos.proof 
158564     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 361.9ns 
158566     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
161657     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.09s 
161658     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdiv_uniquePosPos 
162637     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdiv_uniquePosPos 
162662     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 20.68ms 
162664     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdiv_uniquePosNeg.proof 
162664     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 108.4ns 
162665     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
165708     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.04s 
165708     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdiv_uniquePosNeg 
166688     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdiv_uniquePosNeg 
166714     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 22.5ms 
166715     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdiv_uniqueNegPos.proof 
166715     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 101.3ns 
166716     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
169749     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.03s 
169749     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdiv_uniqueNegPos 
170732     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdiv_uniqueNegPos 
170756     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 19.77ms 
170757     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdiv_uniqueNegNeg.proof 
170757     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 112.2ns 
170758     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
173801     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.04s 
173801     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdiv_uniqueNegNeg 
174771     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdiv_uniqueNegNeg 
174793     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 18.67ms 
174795     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdivMultDenom1.proof 
174795     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 96.9ns 
174796     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
177848     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.05s 
177849     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdivMultDenom1 
178870     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdivMultDenom1 
178923     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 46.57ms 
178925     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdivMultDenom2.proof 
178925     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 79.4ns 
178926     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
181957     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.03s 
181957     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdivMultDenom2 
182929     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdivMultDenom2 
182932     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.54ms 
182934     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_mod_geZero.proof 
182934     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 74.2ns 
182935     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
185945     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.01s 
185945     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: mod_geZero 
186929     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: mod_geZero 
186934     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.1ms 
186936     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_mod_lessDenom.proof 
186936     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 89.8ns 
186937     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
189994     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.06s 
189994     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: mod_lessDenom 
190996     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: mod_lessDenom 
191006     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 7.54ms 
191009     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmod_NumPos.proof 
191009     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 318.1ns 
191010     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
194113     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.1s 
194113     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmod_NumPos 
195084     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmod_NumPos 
195094     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 7.54ms 
195095     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmod_NumNeg.proof 
195096     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 75.4ns 
195096     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
198144     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.05s 
198144     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmod_NumNeg 
199123     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmod_NumNeg 
199147     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 19.96ms 
199148     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmod_geZero.proof 
199149     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 93.6ns 
199150     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
202189     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.04s 
202189     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmod_geZero 
203187     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmod_geZero 
203197     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 7.26ms 
203199     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmodNumZero.proof 
203200     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 105.7ns 
203201     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
206217     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.02s 
206217     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmodNumZero 
207224     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmodNumZero 
207228     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.76ms 
207238     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmod_pulloutminusNum.proof 
207240     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 1.75ms 
207241     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
210302     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.06s 
210302     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmod_pulloutminusNum 
211291     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmod_pulloutminusNum 
211295     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.05ms 
211297     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmod_pulloutminusDenom.proof 
211298     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 102.5ns 
211298     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
214366     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.07s 
214366     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmod_pulloutminusDenom 
215327     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmod_pulloutminusDenom 
215332     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.49ms 
215334     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmodUnique1.proof 
215334     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 416.2ns 
215336     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
218376     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.04s 
218376     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmodUnique1 
219353     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmodUnique1 
219466     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 103.34ms 
219470     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmodUnique2.proof 
219470     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 120.5ns 
219471     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
222509     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.04s 
222509     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmodUnique2 
223492     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmodUnique2 
223607     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 102.71ms 
223610     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_intDivRem.proof 
223610     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 287.2ns 
223611     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
226617     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.01s 
226617     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: intDivRem 
227594     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: intDivRem 
227599     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.14ms 
227600     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmodjmod.proof 
227600     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 74.5ns 
227601     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
230637     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.04s 
230638     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmodjmod 
231632     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmodjmod 
231672     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 35.21ms 
231674     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmodDivisible.proof 
231674     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 99.5ns 
231675     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
234710     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.04s 
234710     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmodDivisible 
235651     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmodDivisible 
235684     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 28.6ms 
235685     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmodDivisibleRep.proof 
235685     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 72.8ns 
235686     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
238728     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.04s 
238728     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmodDivisibleRep 
239696     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmodDivisibleRep 
239700     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.43ms 
239701     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdivAddMultDenom.proof 
239701     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 61.1ns 
239703     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
242722     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.02s 
242723     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdivAddMultDenom 
243702     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdivAddMultDenom 
243874     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 156.13ms 
243884     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmodAltZero.proof 
243884     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 289ns 
243885     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
246885     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3s 
246886     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmodAltZero 
247866     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmodAltZero 
247878     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 8.65ms 
247880     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmodAddMultDenomZero.proof 
247880     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 241.2ns 
247881     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
250892     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.01s 
250892     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmodAddMultDenomZero 
251911     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmodAddMultDenomZero 
251919     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 6.27ms 
251921     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_polyDiv_zero.proof 
251921     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 93.9ns 
251922     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
254946     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.02s 
254946     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: polyDiv_zero 
255926     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: polyDiv_zero 
255950     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 16.97ms 
255952     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_polyMod_ltdivDenom.proof 
255952     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 175.5ns 
255953     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
258955     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3s 
258956     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: polyMod_ltdivDenom 
259937     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: polyMod_ltdivDenom 
259952     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 7.39ms 
259955     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_empty.proof 
259955     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 63.7ns 
259956     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
262918     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.96s 
262918     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_empty 
263907     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_empty 
263911     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.81ms 
263912     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_induction_upper.proof 
263912     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 67.1ns 
263913     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
266923     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.01s 
266923     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_upper 
267901     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_induction_upper 
267906     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.66ms 
267907     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_induction_lower.proof 
267907     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 68.5ns 
267908     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
270946     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.04s 
270946     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_lower 
271920     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_induction_lower 
271942     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 18.06ms 
271944     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_bounds.proof 
271944     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 74.5ns 
271945     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
274997     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.05s 
274997     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_bounds 
275948     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_bounds 
275966     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 14.32ms 
275967     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_bounds2.proof 
275967     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 63.5ns 
275968     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
278997     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.03s 
278997     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_bounds2 
279996     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_bounds2 
280013     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 14.3ms 
280014     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_induction_upper2.proof 
280014     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 73.3ns 
280015     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
283130     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.11s 
283130     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_upper2 
284127     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_induction_upper2 
284133     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.52ms 
284138     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_induction_upper_concrete.proof 
284138     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 247ns 
284139     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
287141     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3s 
287141     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_upper_concrete 
288118     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_induction_upper_concrete 
288122     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.82ms 
288124     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_induction_upper_concrete_2.proof 
288124     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 61.5ns 
288124     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
291170     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.05s 
291171     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_upper_concrete_2 
292153     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_induction_upper_concrete_2 
292159     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.05ms 
292161     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_induction_upper2_concrete.proof 
292161     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 79.4ns 
292162     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
295224     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.06s 
295225     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_upper2_concrete 
296179     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_induction_upper2_concrete 
296182     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.16ms 
296184     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_induction_lower_concrete.proof 
296184     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 77.9ns 
296185     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
299192     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.01s 
299192     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_lower_concrete 
300161     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_induction_lower_concrete 
300164     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 572.1ns 
300165     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_induction_lower2.proof 
300165     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 104.4ns 
300166     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
303194     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.03s 
303194     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_lower2 
304180     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_induction_lower2 
304185     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.35ms 
304186     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_induction_lower2_concrete.proof 
304186     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 94.7ns 
304187     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
307211     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.02s 
307211     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_lower2_concrete 
308180     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_induction_lower2_concrete 
308183     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 960.4ns 
308184     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_positive.proof 
308184     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 58.5ns 
308185     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
311237     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.05s 
311237     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_positive 
312278     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_positive 
312327     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 45.32ms 
312330     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_upper_bound.proof 
312331     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 237.3ns 
312332     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
315372     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.04s 
315372     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_upper_bound 
316353     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_upper_bound 
316406     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 48.26ms 
316408     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_lower_bound.proof 
316408     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 65.8ns 
316409     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
319526     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.12s 
319526     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_lower_bound 
320497     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_lower_bound 
320527     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 26.5ms 
320529     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_positive_lower_bound_element.proof 
320529     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 58.9ns 
320530     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
323675     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.15s 
323676     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_positive_lower_bound_element 
324702     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_positive_lower_bound_element 
324744     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 35.87ms 
324750     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_sub_same_index.proof 
324751     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 273.5ns 
324754     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
327963     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.21s 
327963     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_sub_same_index 
328990     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_sub_same_index 
329016     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 21.74ms 
329017     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_less_same_index.proof 
329017     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 69.7ns 
329019     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
332204     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.19s 
332204     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_less_same_index 
333237     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_less_same_index 
333288     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 45.48ms 
333290     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_equal_except_one_index.proof 
333290     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 81.6ns 
333291     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
336375     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.08s 
336375     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_equal_except_one_index 
337346     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_equal_except_one_index 
337371     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 20.28ms 
337373     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_is_max.proof 
337373     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 77.7ns 
337374     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
340563     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.19s 
340563     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_is_max 
341589     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_is_max 
341610     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 17.1ms 
341612     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_is_max2.proof 
341612     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 68.2ns 
341613     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
344726     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.11s 
344726     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_is_max2 
345748     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_is_max2 
345769     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 17.35ms 
345771     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_is_max3.proof 
345771     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 70.7ns 
345772     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
348935     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.16s 
348935     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_is_max3 
349981     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_is_max3 
350002     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 17.25ms 
350004     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_is_max4.proof 
350004     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 87ns 
350005     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
353216     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.21s 
353216     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_is_max4 
354234     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_is_max4 
354260     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 22.08ms 
354262     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_lt_max.proof 
354262     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 91.5ns 
354263     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
357459     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.2s 
357460     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_lt_max 
358459     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_lt_max 
358483     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 20.15ms 
358485     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_lt_max2.proof 
358485     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 83ns 
358486     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
361678     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.19s 
361678     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_lt_max2 
362700     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_lt_max2 
362725     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 20.49ms 
362727     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_lt_max3.proof 
362727     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 89.4ns 
362728     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
365938     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.21s 
365938     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_lt_max3 
366969     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_lt_max3 
366991     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 17.98ms 
366993     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_lt_max4.proof 
366993     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 88.2ns 
366994     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
370154     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.16s 
370155     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_lt_max4 
371179     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_lt_max4 
371200     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 16.83ms 
371202     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_gt0.proof 
371202     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 816.71ns 
371203     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
374426     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.22s 
374426     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_gt0 
375447     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_gt0 
375473     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 22.23ms 
375475     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_gt0_alt.proof 
375475     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 103.6ns 
375478     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
378695     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.22s 
378696     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_gt0_alt 
379702     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_gt0_alt 
379726     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 20.21ms 
379728     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_add_concrete.proof 
379728     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 91.9ns 
379729     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
382913     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.18s 
382914     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_add_concrete 
383936     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_add_concrete 
383944     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 5.11ms 
383945     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bprod/Taclet_bprod_all_positive.proof 
383946     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 68.5ns 
383946     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
387162     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.22s 
387162     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bprod_all_positive 
388193     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bprod_all_positive 
388210     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 13.59ms 
388213     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bprod/Taclet_bprod_split.proof 
388213     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 71.2ns 
388214     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
391389     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.17s 
391389     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bprod_split 
392430     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bprod_split 
392435     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.38ms 
392437     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powConcrete0.proof 
392437     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 64.4ns 
392438     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
395650     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.21s 
395650     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powConcrete0 
396683     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powConcrete0 
396686     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 825.51ns 
396688     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powConcrete1.proof 
396688     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 77.1ns 
396689     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
399883     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.19s 
399884     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powConcrete1 
400891     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powConcrete1 
400895     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 927.91ns 
400898     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powSplitFactor.proof 
400898     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 260.9ns 
400899     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
404101     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.2s 
404102     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powSplitFactor 
405130     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powSplitFactor 
405138     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.88ms 
405139     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powAdd.proof 
405139     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 76.1ns 
405140     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
408378     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.24s 
408380     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powAdd 
409417     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powAdd 
409432     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.72ms 
409434     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powMono.proof 
409434     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 63.8ns 
409435     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
412606     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.17s 
412606     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powMono 
413623     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powMono 
413637     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 11.19ms 
413639     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powMonoConcrete.proof 
413639     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 87.8ns 
413640     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
416892     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.25s 
416892     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powMonoConcrete 
417937     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powMonoConcrete 
417942     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.2ms 
417943     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powMonoConcreteRight.proof 
417943     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 70.9ns 
417944     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
421099     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.16s 
421100     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powMonoConcreteRight 
422153     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powMonoConcreteRight 
422156     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 644.3ns 
422157     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powPositive.proof 
422157     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 70.7ns 
422158     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
425336     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.18s 
425336     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powPositive 
426356     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powPositive 
426363     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.99ms 
426365     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powPositiveConcrete.proof 
426365     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 76.6ns 
426366     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
429560     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.19s 
429560     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powPositiveConcrete 
430591     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powPositiveConcrete 
430594     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 774.3ns 
430595     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powGeq1Concrete.proof 
430596     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 64.4ns 
430596     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
433793     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.2s 
433794     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powGeq1Concrete 
434828     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powGeq1Concrete 
434831     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 750.8ns 
434832     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_pow2InIntLower.proof 
434832     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 61.1ns 
434833     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
438034     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.2s 
438034     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: pow2InIntLower 
439019     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: pow2InIntLower 
439021     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 695.11ns 
439023     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_pow2InIntUpper.proof 
439023     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 72.2ns 
439024     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
442214     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.19s 
442214     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: pow2InIntUpper 
443224     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: pow2InIntUpper 
443229     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.29ms 
443230     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logSelfConcrete.proof 
443231     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 77.7ns 
443231     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
446436     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.2s 
446436     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logSelfConcrete 
447479     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logSelfConcrete 
447490     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 7.49ms 
447491     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_log1Concrete.proof 
447492     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 78ns 
447492     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
450682     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.19s 
450682     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: log1Concrete 
451720     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: log1Concrete 
451725     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.58ms 
451727     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logProduct.proof 
451727     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 76.9ns 
451728     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
454925     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.2s 
454925     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logProduct 
455940     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logProduct 
455949     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 5.56ms 
455951     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logTimesBaseConcrete.proof 
455951     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 73.3ns 
455952     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
459223     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.27s 
459223     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logTimesBaseConcrete 
460267     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logTimesBaseConcrete 
460273     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.87ms 
460274     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logProdIdentity.proof 
460275     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 80.5ns 
460275     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
463479     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.2s 
463479     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logProdIdentity 
464501     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logProdIdentity 
464519     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 14.47ms 
464521     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logProdIdentityConcrete.proof 
464521     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 76.3ns 
464522     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
467624     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.1s 
467624     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logProdIdentityConcrete 
468630     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logProdIdentityConcrete 
468635     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.4ms 
468636     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logPowIdentity.proof 
468636     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 58.9ns 
468637     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
471700     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.06s 
471700     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logPowIdentity 
472664     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logPowIdentity 
472668     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.42ms 
472669     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logPowIdentityConcrete.proof 
472669     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 58.5ns 
472670     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
475703     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.03s 
475704     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logPowIdentityConcrete 
476684     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logPowIdentityConcrete 
476688     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.97ms 
476690     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logPositive.proof 
476690     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 90.9ns 
476691     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
479740     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.05s 
479740     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logPositive 
480739     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logPositive 
480758     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 15.57ms 
480759     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logPositiveConcrete.proof 
480759     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 66.3ns 
480760     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
483820     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.06s 
483820     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logPositiveConcrete 
484799     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logPositiveConcrete 
484804     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 388.4ns 
484806     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logMono.proof 
484806     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 71.8ns 
484807     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
487786     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.98s 
487786     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logMono 
488760     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logMono 
488807     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 41.99ms 
488810     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logMonoConcrete.proof 
488810     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 79.8ns 
488811     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
491879     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.07s 
491879     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logMonoConcrete 
492886     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logMonoConcrete 
492891     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.02ms 
492892     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powLogLess.proof 
492892     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 59.6ns 
492893     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
495974     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.08s 
495974     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powLogLess 
496982     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powLogLess 
497005     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 18.37ms 
497009     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powLogMore2.proof 
497009     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 226.4ns 
497012     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
500131     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.12s 
500132     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powLogMore2 
501104     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powLogMore2 
501124     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 17.17ms 
501125     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logLessThanPow.proof 
501125     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 84.4ns 
501126     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
504231     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.11s 
504231     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logLessThanPow 
505232     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logLessThanPow 
505260     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 24.01ms 
505262     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logLessThanPowConcrete.proof 
505262     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 76.2ns 
505263     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
508429     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.17s 
508429     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logLessThanPowConcrete 
509468     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logLessThanPowConcrete 
509470     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 643.8ns 
509472     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logSqueeze.proof 
509472     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 59ns 
509473     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
512684     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.21s 
512685     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logSqueeze 
513718     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logSqueeze 
513725     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.38ms 
513727     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/booleanRules/Taclet_ifthenelse_equals.proof 
513727     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 57.5ns 
513728     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
516878     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.15s 
516878     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: ifthenelse_equals 
517888     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: ifthenelse_equals 
517892     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.88ms 
517893     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/booleanRules/Taclet_ifthenelse_equals_1.proof 
517893     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 66.2ns 
517894     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
521125     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.23s 
521125     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: ifthenelse_equals_1 
522198     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: ifthenelse_equals_1 
522201     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.06ms 
522203     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/booleanRules/Taclet_ifthenelse_equals_2.proof 
522203     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 81.6ns 
522204     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
525345     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.14s 
525345     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: ifthenelse_equals_2 
526359     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: ifthenelse_equals_2 
526362     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.05ms 
526364     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/locSet/Taclet_disjointWithSingleton1.proof 
526364     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 60.5ns 
526364     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
529547     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.18s 
529547     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: disjointWithSingleton1 
530579     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: disjointWithSingleton1 
530583     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.58ms 
530585     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/locSet/Taclet_disjointWithSingleton2.proof 
530585     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 59.7ns 
530586     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
533681     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.1s 
533681     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: disjointWithSingleton2 
534654     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: disjointWithSingleton2 
534658     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.25ms 
534659     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/locSet/Taclet_disjointArrayRanges.proof 
534659     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 72.7ns 
534660     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
537700     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.04s 
537700     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: disjointArrayRanges 
538775     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: disjointArrayRanges 
538787     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 8.3ms 
538789     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/locSet/Taclet_disjointArrayRangeAllFields1.proof 
538789     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 67.7ns 
538789     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
541888     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.1s 
541888     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: disjointArrayRangeAllFields1 
542919     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: disjointArrayRangeAllFields1 
542930     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 8.72ms 
542932     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/locSet/Taclet_disjointArrayRangeAllFields2.proof 
542932     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 120.5ns 
542933     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
546116     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.18s 
546116     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: disjointArrayRangeAllFields2 
547194     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: disjointArrayRangeAllFields2 
547203     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 6.79ms 
547205     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqSelfDefinition.proof 
547205     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 69.7ns 
547206     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
550518     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.31s 
550518     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqSelfDefinition 
551597     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqSelfDefinition 
551608     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 8.06ms 
551610     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqOutsideValue.proof 
551610     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 79ns 
551611     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
554824     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.21s 
554824     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqOutsideValue 
555884     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqOutsideValue 
555889     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.87ms 
555891     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_castedGetAny.proof 
555891     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 84ns 
555892     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
559120     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.23s 
559121     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: castedGetAny 
560144     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: castedGetAny 
560184     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.74ms 
560187     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqGetAlphaCast.proof 
560187     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 269.8ns 
560188     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
563371     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.18s 
563371     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqGetAlphaCast 
564427     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqGetAlphaCast 
564430     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.11ms 
564432     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqSingleton.proof 
564432     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 80.1ns 
564433     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
567639     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.21s 
567639     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqSingleton 
568704     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqSingleton 
568707     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.72ms 
568709     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqSingletonConcrete.proof 
568709     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 74.5ns 
568710     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
571903     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.19s 
571903     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqSingletonConcrete 
572949     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqSingletonConcrete 
572953     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.24ms 
572955     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqConcat.proof 
572956     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 254.3ns 
572957     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
576211     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.25s 
576211     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqConcat 
577265     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqConcat 
577279     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 10.79ms 
577281     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqSub.proof 
577281     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 64.2ns 
577281     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
580455     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.17s 
580455     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqSub 
581501     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqSub 
581506     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.92ms 
581507     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqReverse.proof 
581508     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 73.1ns 
581509     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
584730     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.22s 
584731     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqReverse 
585786     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqReverse 
585794     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 5.01ms 
585795     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqEmpty.proof 
585795     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 62.9ns 
585796     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
589055     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.26s 
589055     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqEmpty 
590128     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqEmpty 
590132     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.61ms 
590133     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqSingleton.proof 
590133     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 66.8ns 
590134     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
593311     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.18s 
593311     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqSingleton 
594375     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqSingleton 
594378     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 833.4ns 
594380     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqConcat.proof 
594380     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 71.9ns 
594381     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
597568     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.19s 
597568     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqConcat 
598599     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqConcat 
598603     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.97ms 
598605     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqSub.proof 
598605     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 241.4ns 
598606     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
601643     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.04s 
601643     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqSub 
602654     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqSub 
602657     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.12ms 
602658     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqReverse.proof 
602658     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 80.1ns 
602659     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
605705     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.05s 
605706     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqReverse 
606707     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqReverse 
606711     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.83ms 
606714     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_equalityToSeqGetAndSeqLenLeft.proof 
606714     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 217.4ns 
606715     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
609710     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3s 
609711     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: equalityToSeqGetAndSeqLenLeft 
610702     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: equalityToSeqGetAndSeqLenLeft 
610705     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.39ms 
610707     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_equalityToSeqGetAndSeqLenRight.proof 
610707     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 57.6ns 
610708     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
613782     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.07s 
613782     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: equalityToSeqGetAndSeqLenRight 
614777     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: equalityToSeqGetAndSeqLenRight 
614782     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.74ms 
614784     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqSingletonEQ.proof 
614784     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 53.5ns 
614784     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
617781     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3s 
617782     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqSingletonEQ 
618760     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqSingletonEQ 
618763     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.05ms 
618764     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqConcatEQ.proof 
618764     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 66.8ns 
618765     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
621801     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.04s 
621801     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqConcatEQ 
622789     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqConcatEQ 
622801     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 9.48ms 
622803     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqSubEQ.proof 
622803     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 75.4ns 
622804     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
625804     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3s 
625804     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqSubEQ 
626817     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqSubEQ 
626819     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 612.2ns 
626821     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqReverseEQ.proof 
626821     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 68ns 
626822     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
629811     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.99s 
629811     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqReverseEQ 
630804     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqReverseEQ 
630812     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 5.15ms 
630813     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqEmptyEQ.proof 
630813     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 70.5ns 
630814     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
633909     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.09s 
633909     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqEmptyEQ 
634915     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqEmptyEQ 
634918     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.1ms 
634920     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqSingletonEQ.proof 
634920     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 72.6ns 
634921     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
637908     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.99s 
637908     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqSingletonEQ 
638901     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqSingletonEQ 
638904     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 932.01ns 
638905     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqConcatEQ.proof 
638905     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 66.1ns 
638906     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
641959     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.05s 
641959     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqConcatEQ 
642982     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqConcatEQ 
642987     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.11ms 
642991     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqSubEQ.proof 
642991     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 231.9ns 
642992     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
646067     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.08s 
646068     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqSubEQ 
647065     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqSubEQ 
647068     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.23ms 
647070     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqReverseEQ.proof 
647070     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 51.9ns 
647070     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
650079     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.01s 
650080     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqReverseEQ 
651105     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqReverseEQ 
651109     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.93ms 
651110     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqDefEQ.proof 
651110     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 69.1ns 
651111     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
654157     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.05s 
654158     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqDefEQ 
655145     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqDefEQ 
655148     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.63ms 
655150     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqDefEQ.proof 
655150     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 58.4ns 
655151     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
658163     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.01s 
658163     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqDefEQ 
659187     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqDefEQ 
659193     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.5ms 
659195     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqConcatWithSeqEmpty1.proof 
659195     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 68.5ns 
659195     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
662313     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.12s 
662314     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqConcatWithSeqEmpty1 
663295     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqConcatWithSeqEmpty1 
663304     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 7.2ms 
663306     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqConcatWithSeqEmpty2.proof 
663306     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 99.8ns 
663307     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
666310     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3s 
666310     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqConcatWithSeqEmpty2 
667323     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqConcatWithSeqEmpty2 
667335     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 9.27ms 
667336     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqReverseOfSeqEmpty.proof 
667336     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 69.6ns 
667337     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
670355     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.02s 
670355     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqReverseOfSeqEmpty 
671361     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqReverseOfSeqEmpty 
671369     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 6.15ms 
671371     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_subSeqComplete.proof 
671371     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 68.8ns 
671372     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
674439     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.07s 
674440     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: subSeqComplete 
675453     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: subSeqComplete 
675460     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 5.41ms 
675462     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_subSeqTailR.proof 
675462     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 80.4ns 
675463     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
678439     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.98s 
678439     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: subSeqTailR 
679428     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: subSeqTailR 
679443     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 12.54ms 
679445     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_subSeqTailL.proof 
679445     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 74.4ns 
679446     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
682467     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.02s 
682467     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: subSeqTailL 
683474     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: subSeqTailL 
683489     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 11.73ms 
683490     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_subSeqTailEQR.proof 
683490     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 89.1ns 
683491     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
686696     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.2s 
686696     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: subSeqTailEQR 
687768     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: subSeqTailEQR 
687782     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 10.84ms 
687784     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_subSeqTailEQL.proof 
687784     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 109.7ns 
687785     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
690970     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.18s 
690970     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: subSeqTailEQL 
692007     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: subSeqTailEQL 
692017     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 7.13ms 
692018     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDef_split.proof 
692019     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 74.7ns 
692019     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
695257     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.24s 
695257     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_split 
696321     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDef_split 
696350     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 25.2ms 
696352     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDef_induction_upper.proof 
696352     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 68.8ns 
696353     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
699720     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.37s 
699720     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_induction_upper 
700765     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDef_induction_upper 
700797     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 27.13ms 
700799     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDef_induction_upper_concrete.proof 
700799     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 82.9ns 
700800     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
704050     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.25s 
704050     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_induction_upper_concrete 
705131     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDef_induction_upper_concrete 
705166     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 30.66ms 
705168     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDef_induction_lower.proof 
705169     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 94.8ns 
705170     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
708517     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.35s 
708517     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_induction_lower 
709574     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDef_induction_lower 
709601     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 23.27ms 
709604     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDef_induction_lower_concrete.proof 
709605     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 125.9ns 
709605     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
712822     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.22s 
712822     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_induction_lower_concrete 
713872     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDef_induction_lower_concrete 
713902     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 26.33ms 
713904     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDef_split_in_three.proof 
713904     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 86.2ns 
713905     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
717134     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.23s 
717134     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_split_in_three 
718181     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDef_split_in_three 
718255     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 64.39ms 
718257     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDef_empty.proof 
718257     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 63.1ns 
718258     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
721476     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.22s 
721476     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_empty 
722521     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDef_empty 
722527     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.24ms 
722529     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDef_one_summand.proof 
722530     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 81.4ns 
722530     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
725741     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.21s 
725742     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_one_summand 
726797     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDef_one_summand 
726804     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 5.02ms 
726806     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDef_lower_equals_upper.proof 
726806     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 92.3ns 
726807     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
729966     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.16s 
729966     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_lower_equals_upper 
731035     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDef_lower_equals_upper 
731040     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.72ms 
731041     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDefOfSeq.proof 
731041     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 85.6ns 
731042     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
734209     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.17s 
734209     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDefOfSeq 
735246     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDefOfSeq 
735265     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 15.27ms 
735268     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqSelfDefinitionEQ2.proof 
735269     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 744ns 
735269     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
738447     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.18s 
738447     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqSelfDefinitionEQ2 
739477     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqSelfDefinitionEQ2 
739486     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 6.03ms 
739488     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_indexOfSeqSingleton.proof 
739488     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 63.8ns 
739488     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
742681     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.19s 
742681     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: indexOfSeqSingleton 
743724     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: indexOfSeqSingleton 
743729     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.44ms 
743731     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_indexOfSeqConcatFirst.proof 
743731     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 93.3ns 
743732     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
746918     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.19s 
746918     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: indexOfSeqConcatFirst 
747947     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: indexOfSeqConcatFirst 
747962     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 11.78ms 
747964     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_indexOfSeqConcatSecond.proof 
747964     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 81.1ns 
747965     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
751102     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.14s 
751102     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: indexOfSeqConcatSecond 
752136     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: indexOfSeqConcatSecond 
752153     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 12.16ms 
752154     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_indexOfSeqSub.proof 
752154     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 76.9ns 
752155     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
755304     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.15s 
755305     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: indexOfSeqSub 
756366     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: indexOfSeqSub 
756385     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 16.06ms 
756387     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfArray2seq.proof 
756387     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 64.1ns 
756388     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
759544     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.16s 
759544     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfArray2seq 
760592     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfArray2seq 
760596     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.37ms 
760598     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getAnyOfArray2seq.proof 
760598     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 81.8ns 
760599     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
763773     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.17s 
763773     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getAnyOfArray2seq 
764827     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getAnyOfArray2seq 
764835     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 5.76ms 
764838     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfArray2seq.proof 
764838     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 286.4ns 
764839     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
768162     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.32s 
768162     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfArray2seq 
769316     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfArray2seq 
769324     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 5.48ms 
769325     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_getAnyOfNPermInv.proof 
769325     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 74.9ns 
769326     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
772532     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.21s 
772532     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getAnyOfNPermInv 
773593     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getAnyOfNPermInv 
773600     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.43ms 
773602     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqNPermRange.proof 
773602     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 74.1ns 
773603     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
776658     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.06s 
776659     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqNPermRange 
777666     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqNPermRange 
777735     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 59.41ms 
777737     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermTrans.proof 
777737     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 72.9ns 
777738     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
780796     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.06s 
780796     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermTrans 
781836     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermTrans 
781863     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 21.94ms 
781864     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermRefl.proof 
781864     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 65.2ns 
781865     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
784883     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.02s 
784883     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermRefl 
785882     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermRefl 
785897     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 12.51ms 
785899     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermSplit.proof 
785899     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 67.5ns 
785900     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
788854     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.95s 
788854     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermSplit 
789822     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermSplit 
789824     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 291.7ns 
789826     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqNPermRight.proof 
789826     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 55.1ns 
789827     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
792779     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.95s 
792779     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqNPermRight 
793793     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqNPermRight 
793916     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 107.15ms 
793918     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermFromSwap.proof 
793918     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 73.1ns 
793919     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
796909     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.99s 
796909     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermFromSwap 
797927     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermFromSwap 
797977     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 43.96ms 
797979     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermTransAlt0.proof 
797979     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 56.3ns 
797980     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
801075     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.09s 
801075     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermTransAlt0 
802111     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermTransAlt0 
802114     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 694.71ns 
802116     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermTransAlt1.proof 
802117     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 258.4ns 
802119     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
805217     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.1s 
805217     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermTransAlt1 
806243     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermTransAlt1 
806246     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 282.7ns 
806247     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermTransAlt2.proof 
806247     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 64.8ns 
806248     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
809308     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.06s 
809309     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermTransAlt2 
810356     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermTransAlt2 
810358     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 356.5ns 
810361     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermTransAlt3.proof 
810362     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 290.8ns 
810363     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
813371     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.01s 
813371     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermTransAlt3 
814382     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermTransAlt3 
814384     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 572.2ns 
814385     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermForall.proof 
814386     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 70.3ns 
814386     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
817434     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.05s 
817434     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermForall 
818446     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermForall 
818549     INFO  Test worker     d.u.i.k.s.SMTFocusResults Analyzing unsat core: (L_1 L_3 L_4) 
818564     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 115.1ms 
818567     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermExists.proof 
818567     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 230.3ns 
818569     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
821655     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.09s 
821655     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermExists 
822677     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermExists 
822736     INFO  Test worker     d.u.i.k.s.SMTFocusResults Analyzing unsat core: (L_1 L_3 L_5 L_6 L_7) 
822738     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 53.79ms 
822740     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm2/Taclet_schiffl_lemma_2.proof 
822740     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 67.4ns 
822741     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
825811     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.07s 
825811     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: schiffl_lemma_2 
826843     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: schiffl_lemma_2 
826845     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.1ns 
826888     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [1] goal: 0, source line: 49, command: 'macro split-prop' 
826924     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [2] goal: 3, source line: 50, command: 'rule allRight' 
826942     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [3] goal: 4, source line: 51, command: 'rule allRight' 
826946     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [4] goal: 5, source line: 52, command: 'macro split-prop' 
826958     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [5] goal: 11, source line: 53, command: 'rule 'seqPermDefLeft'' 
826959     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [6] goal: 12, source line: 54, command: 'rule 'andLeft'' 
826961     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [7] goal: 13, source line: 55, command: 'rule 'exLeft'' 
826963     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [8] goal: 14, source line: 56, command: 'macro split-prop' 
826967     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [9] goal: 16, source line: 57, command: 'rule  seqNPermRange' 
826969     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' 
826971     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [11] goal: 18, source line: 60, command: 'rule impLeft' 
826975     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [12] goal: 19, source line: 61, command: 'tryclose branch' 
827248     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [13] goal: 20, source line: 62, command: 'rule andLeft' 
827251     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [14] goal: 97, source line: 63, command: 'rule andLeft' 
827254     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' 
827255     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [16] goal: 99, source line: 66, command: 'rule impLeft' 
827257     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [17] goal: 100, source line: 67, command: 'tryclose branch' 
827446     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [18] goal: 101, source line: 68, command: 'rule andLeft' 
827447     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [19] goal: 188, source line: 69, command: 'rule andLeft' 
827448     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [20] goal: 189, source line: 70, command: 'rule seqNPermDefLeft' 
827449     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' 
827450     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [22] goal: 191, source line: 73, command: 'rule impLeft' 
827452     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [23] goal: 192, source line: 74, command: 'tryclose branch' 
827645     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [24] goal: 193, source line: 75, command: 'rule exLeft' 
827646     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [25] goal: 310, source line: 76, command: 'rule andLeft' 
827647     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [26] goal: 311, source line: 77, command: 'rule andLeft' 
827648     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' 
827649     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [28] goal: 313, source line: 80, command: 'rule impLeft' 
827650     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [29] goal: 314, source line: 81, command: 'tryclose branch' 
827784     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [30] goal: 315, source line: 82, command: 'rule exLeft' 
827786     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [31] goal: 420, source line: 83, command: 'rule andLeft' 
827787     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [32] goal: 421, source line: 84, command: 'rule andLeft' 
827788     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' 
827788     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [34] goal: 423, source line: 87, command: 'rule impLeft' 
827790     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [35] goal: 424, source line: 88, command: 'tryclose branch' 
827797     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [36] goal: 425, source line: 89, command: 'rule andLeft' 
827798     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [37] goal: 434, source line: 90, command: 'rule andLeft' 
827800     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' 
827800     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' 
827801     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [40] goal: 437, source line: 94, command: 'rule impLeft' 
827802     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [41] goal: 438, source line: 95, command: 'tryclose branch' 
827809     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [42] goal: 439, source line: 96, command: 'rule andLeft' 
827810     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [43] goal: 448, source line: 97, command: 'rule andLeft' 
827811     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' 
827812     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [45] goal: 450, source line: 99, command: 'instantiate var=iv  with='v_x_0'' 
827812     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [46] goal: 451, source line: 101, command: 'rule impLeft' 
827813     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [47] goal: 452, source line: 102, command: 'tryclose branch' 
827958     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [48] goal: 453, source line: 103, command: 'instantiate var=iv  with='v_y_0'' 
827959     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [49] goal: 562, source line: 105, command: 'rule impLeft' 
827960     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [50] goal: 563, source line: 106, command: 'tryclose branch' 
828103     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [51] goal: 564, source line: 107, command: 'cut 'v_x_0 = v_y_0'' 
828104     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)'' 
828105     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [53] goal: 676, source line: 111, command: 'rule andRight' 
828108     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [54] goal: 677, source line: 113, command: 'rule andRight' 
828108     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [55] goal: 679, source line: 114, command: 'rule andRight' 
828109     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [56] goal: 681, source line: 115, command: 'rule andRight' 
828110     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [57] goal: 683, source line: 116, command: 'rule lenOfSwap' 
828116     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [58] goal: 685, source line: 117, command: 'tryclose branch' 
828120     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [59] goal: 684, source line: 118, command: 'rule seqNPermSwapNPerm' 
828121     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' 
828122     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [61] goal: 688, source line: 121, command: 'instantiate hide var='jv' with='jv_0'' 
828129     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [62] goal: 689, source line: 122, command: 'rule impLeft' 
828130     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [63] goal: 690, source line: 123, command: 'tryclose branch' 
828252     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [64] goal: 691, source line: 124, command: 'tryclose branch' 
828256     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [65] goal: 682, source line: 125, command: 'rule allRight' 
828257     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [66] goal: 796, source line: 127, command: 'rule impRight' 
828258     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [67] goal: 797, source line: 128, command: 'rule andLeft' 
828259     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [68] goal: 798, source line: 129, command: 'instantiate var=iv with='v_iv_0'' 
828259     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [69] goal: 799, source line: 130, command: 'rule impLeft' 
828261     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [70] goal: 800, source line: 131, command: 'tryclose branch' 
828398     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [71] goal: 801, source line: 132, command: 'rule getOfSwap' 
828399     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [72] goal: 912, source line: 133, command: 'rule ifthenelse_negated' 
828400     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [73] goal: 913, source line: 134, command: 'rule ifthenelse_split occ=0' 
828401     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [74] goal: 914, source line: 135, command: 'rule andLeft' 
828402     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [75] goal: 916, source line: 136, command: 'rule andLeft' 
828403     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [76] goal: 917, source line: 137, command: 'rule andLeft' 
828404     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [77] goal: 918, source line: 138, command: 'rule ifthenelse_split occ=0' 
828404     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [78] goal: 919, source line: 139, command: 'tryclose branch' 
828519     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [79] goal: 920, source line: 140, command: 'rule ifthenelse_split occ=0' 
828520     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [80] goal: 1011, source line: 141, command: 'tryclose branch' 
828628     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [81] goal: 1012, source line: 142, command: 'tryclose branch' 
828633     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [82] goal: 915, source line: 143, command: 'tryclose branch' 
828638     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [83] goal: 680, source line: 144, command: 'rule getOfSwap' 
828639     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [84] goal: 1099, source line: 146, command: 'rule ifthenelse_negated' 
828640     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [85] goal: 1100, source line: 147, command: 'rule ifthenelse_split occ=0' 
828641     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [86] goal: 1101, source line: 148, command: 'rule andLeft' 
828642     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [87] goal: 1103, source line: 149, command: 'rule andLeft' 
828642     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [88] goal: 1104, source line: 150, command: 'rule andLeft' 
828643     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [89] goal: 1105, source line: 151, command: 'rule ifthenelse_split occ=0' 
828643     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [90] goal: 1106, source line: 152, command: 'tryclose branch' 
828653     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [91] goal: 1107, source line: 153, command: 'tryclose branch' 
828659     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [92] goal: 1102, source line: 154, command: 'tryclose branch' 
828784     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [93] goal: 678, source line: 155, command: 'rule getOfSwap' 
828785     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [94] goal: 1225, source line: 157, command: 'rule ifthenelse_negated' 
828786     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [95] goal: 1226, source line: 158, command: 'rule ifthenelse_split occ=0' 
828787     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [96] goal: 1227, source line: 159, command: 'rule andLeft' 
828788     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [97] goal: 1229, source line: 160, command: 'rule andLeft' 
828789     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [98] goal: 1230, source line: 161, command: 'rule andLeft' 
828789     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [99] goal: 1231, source line: 162, command: 'rule ifthenelse_split occ=0' 
828790     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [100] goal: 1232, source line: 163, command: 'tryclose branch' 
828860     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [101] goal: 1233, source line: 164, command: 'tryclose branch' 
828867     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [102] goal: 1228, source line: 165, command: 'tryclose branch' 
828993     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]'' 
828994     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [104] goal: 1397, source line: 169, command: 'rule seqNPermInjective' 
828995     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'' 
828997     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'' 
828999     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [107] goal: 1401, source line: 172, command: 'rule impLeft' 
829000     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [108] goal: 1402, source line: 173, command: 'tryclose branch' 
829153     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [109] goal: 1403, source line: 174, command: 'tryclose branch' 
829158     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'' 
829159     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)'' 
829159     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [112] goal: 1536, source line: 179, command: 'rule andRight' 
829161     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [113] goal: 1537, source line: 181, command: 'rule andRight' 
829162     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [114] goal: 1539, source line: 182, command: 'rule andRight' 
829163     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [115] goal: 1541, source line: 183, command: 'rule andRight' 
829163     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [116] goal: 1543, source line: 184, command: 'tryclose branch' 
829175     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [117] goal: 1544, source line: 185, command: 'rule seqNPermSwapNPerm' 
829176     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'' 
829177     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [119] goal: 1559, source line: 188, command: 'instantiate hide var=jv with='jv_1'' 
829178     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [120] goal: 1560, source line: 189, command: 'tryclose branch' 
829339     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [121] goal: 1542, source line: 190, command: 'rule allRight' 
829341     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [122] goal: 1667, source line: 192, command: 'rule impRight' 
829342     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [123] goal: 1668, source line: 193, command: 'rule andLeft' 
829343     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [124] goal: 1669, source line: 194, command: 'instantiate var=iv with='v_iv_0'' 
829344     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [125] goal: 1670, source line: 195, command: 'rule impLeft' 
829345     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [126] goal: 1671, source line: 196, command: 'tryclose branch' 
829474     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [127] goal: 1672, source line: 197, command: 'rule getOfSwap' 
829475     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [128] goal: 1786, source line: 198, command: 'rule ifthenelse_negated' 
829477     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [129] goal: 1787, source line: 199, command: 'rule ifthenelse_split occ=0' 
829478     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [130] goal: 1788, source line: 200, command: 'rule andLeft' 
829479     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [131] goal: 1790, source line: 201, command: 'rule andLeft' 
829480     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [132] goal: 1791, source line: 202, command: 'rule andLeft' 
829481     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [133] goal: 1792, source line: 203, command: 'rule ifthenelse_split occ=0' 
829482     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [134] goal: 1793, source line: 204, command: 'tryclose branch' 
829584     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [135] goal: 1794, source line: 205, command: 'rule ifthenelse_split occ=0' 
829587     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [136] goal: 1885, source line: 206, command: 'tryclose branch' 
829681     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [137] goal: 1886, source line: 207, command: 'instantiate var=iv with='v_y_0'' 
829682     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [138] goal: 1968, source line: 208, command: 'rule impLeft' 
829683     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [139] goal: 1969, source line: 209, command: 'tryclose branch' 
829688     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [140] goal: 1970, source line: 210, command: 'tryclose branch' 
829693     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [141] goal: 1789, source line: 211, command: 'tryclose branch' 
829700     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [142] goal: 1540, source line: 212, command: 'tryclose branch' 
829853     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [143] goal: 1538, source line: 213, command: 'rule getOfSwap' 
829855     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [144] goal: 2097, source line: 215, command: 'rule ifthenelse_negated' 
829856     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [145] goal: 2098, source line: 216, command: 'rule ifthenelse_split occ=0' 
829857     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [146] goal: 2099, source line: 217, command: 'tryclose branch' 
829870     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [147] goal: 2100, source line: 218, command: 'tryclose branch' 
829982     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [148] goal: 1535, source line: 219, command: 'tryclose branch' 
834550     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'' 
834551     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)'' 
834556     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [151] goal: 4268, source line: 226, command: 'rule andRight' 
834558     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [152] goal: 4269, source line: 228, command: 'rule andRight' 
834558     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [153] goal: 4271, source line: 229, command: 'rule andRight' 
834559     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [154] goal: 4273, source line: 230, command: 'rule andRight' 
834559     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [155] goal: 4275, source line: 231, command: 'tryclose branch' 
834570     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [156] goal: 4276, source line: 232, command: 'rule seqNPermSwapNPerm' 
834571     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'' 
834572     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [158] goal: 4288, source line: 235, command: 'instantiate hide var=jv with='jv_0'' 
834573     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [159] goal: 4289, source line: 236, command: 'rule impLeft' 
834574     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [160] goal: 4290, source line: 237, command: 'tryclose branch' 
834696     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [161] goal: 4291, source line: 238, command: 'tryclose branch' 
834701     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [162] goal: 4274, source line: 239, command: 'rule allRight' 
834701     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [163] goal: 4400, source line: 241, command: 'rule impRight' 
834702     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [164] goal: 4401, source line: 242, command: 'rule andLeft' 
834703     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [165] goal: 4402, source line: 243, command: 'instantiate var=iv with='v_iv_0'' 
834704     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [166] goal: 4403, source line: 244, command: 'rule impLeft' 
834704     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [167] goal: 4404, source line: 245, command: 'tryclose branch' 
834832     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [168] goal: 4405, source line: 246, command: 'rule getOfSwap' 
834833     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [169] goal: 4521, source line: 247, command: 'rule ifthenelse_negated' 
834834     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [170] goal: 4522, source line: 248, command: 'rule ifthenelse_split occ=0' 
834836     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [171] goal: 4523, source line: 249, command: 'rule andLeft' 
834837     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [172] goal: 4525, source line: 250, command: 'rule andLeft' 
834837     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [173] goal: 4526, source line: 251, command: 'rule andLeft' 
834838     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [174] goal: 4527, source line: 252, command: 'rule ifthenelse_split occ=0' 
834839     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [175] goal: 4528, source line: 253, command: 'tryclose branch' 
834940     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [176] goal: 4529, source line: 254, command: 'rule ifthenelse_split occ=0' 
834941     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [177] goal: 4622, source line: 255, command: 'tryclose branch' 
835039     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [178] goal: 4623, source line: 256, command: 'tryclose branch' 
835045     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [179] goal: 4524, source line: 257, command: 'tryclose branch' 
835050     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [180] goal: 4272, source line: 258, command: 'rule getOfSwap' 
835051     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [181] goal: 4713, source line: 260, command: 'rule ifthenelse_negated' 
835052     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [182] goal: 4714, source line: 261, command: 'rule ifthenelse_split occ=0' 
835053     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [183] goal: 4715, source line: 262, command: 'tryclose branch' 
835066     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [184] goal: 4716, source line: 263, command: 'tryclose branch' 
835172     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [185] goal: 4270, source line: 264, command: 'rule getOfSwap' 
835173     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [186] goal: 4839, source line: 266, command: 'rule ifthenelse_negated' 
835174     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [187] goal: 4840, source line: 267, command: 'rule ifthenelse_split occ=0' 
835175     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [188] goal: 4841, source line: 268, command: 'tryclose branch' 
835271     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [189] goal: 4842, source line: 269, command: 'tryclose branch' 
835283     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'' 
835283     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)'' 
835284     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [192] goal: 4950, source line: 275, command: 'rule andRight' 
835286     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [193] goal: 4951, source line: 277, command: 'rule andRight' 
835286     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [194] goal: 4953, source line: 278, command: 'rule andRight' 
835287     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [195] goal: 4955, source line: 279, command: 'rule andRight' 
835287     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [196] goal: 4957, source line: 280, command: 'tryclose branch' 
835302     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [197] goal: 4958, source line: 281, command: 'rule seqNPermSwapNPerm' 
835302     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [198] goal: 4977, source line: 283, command: 'instantiate hide var=iv with='jv_0'' 
835303     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'' 
835304     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [200] goal: 4979, source line: 285, command: 'rule impLeft' 
835305     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [201] goal: 4980, source line: 286, command: 'tryclose branch' 
835423     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))'' 
835423     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [203] goal: 5093, source line: 288, command: 'instantiate hide var=iv with='jv_0'' 
835425     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'' 
835428     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [205] goal: 5095, source line: 290, command: 'rule impLeft' 
835429     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [206] goal: 5096, source line: 291, command: 'tryclose branch' 
835549     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [207] goal: 5097, source line: 292, command: 'tryclose branch' 
835554     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [208] goal: 4956, source line: 293, command: 'rule allRight' 
835555     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [209] goal: 5212, source line: 295, command: 'rule impRight' 
835556     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [210] goal: 5213, source line: 296, command: 'rule andLeft' 
835557     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [211] goal: 5214, source line: 297, command: 'instantiate var=iv with='v_iv_0'' 
835557     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [212] goal: 5215, source line: 300, command: 'rule impLeft' 
835558     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [213] goal: 5216, source line: 301, command: 'tryclose branch' 
835691     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [214] goal: 5217, source line: 302, command: 'rule getOfSwap' 
835692     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [215] goal: 5337, source line: 304, command: 'rule ifthenelse_negated' 
835693     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [216] goal: 5338, source line: 305, command: 'rule ifthenelse_split occ=0' 
835694     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [217] goal: 5339, source line: 306, command: 'rule andLeft' 
835695     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [218] goal: 5341, source line: 307, command: 'rule andLeft' 
835696     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [219] goal: 5342, source line: 308, command: 'rule andLeft' 
835696     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [220] goal: 5343, source line: 309, command: 'rule ifthenelse_split occ=0' 
835697     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [221] goal: 5344, source line: 310, command: 'rule getOfSwap' 
835698     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [222] goal: 5346, source line: 311, command: 'rule ifthenelse_negated' 
835698     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [223] goal: 5347, source line: 312, command: 'rule ifthenelse_split occ=0' 
835699     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [224] goal: 5348, source line: 313, command: 'rule andLeft' 
835700     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [225] goal: 5350, source line: 314, command: 'rule andLeft' 
835701     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [226] goal: 5351, source line: 315, command: 'rule andLeft' 
835701     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [227] goal: 5352, source line: 316, command: 'rule ifthenelse_split occ=0' 
835702     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [228] goal: 5353, source line: 317, command: 'tryclose branch' 
835873     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [229] goal: 5354, source line: 318, command: 'rule ifthenelse_split occ=0' 
835875     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [230] goal: 5463, source line: 319, command: 'tryclose branch' 
835882     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [231] goal: 5464, source line: 320, command: 'tryclose branch' 
835982     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [232] goal: 5349, source line: 321, command: 'tryclose branch' 
836089     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [233] goal: 5345, source line: 322, command: 'rule ifthenelse_split' 
836090     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [234] goal: 5660, source line: 324, command: 'rule getOfSwap' 
836091     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [235] goal: 5662, source line: 325, command: 'rule ifthenelse_negated' 
836092     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [236] goal: 5663, source line: 326, command: 'rule ifthenelse_split occ=0' 
836093     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [237] goal: 5664, source line: 327, command: 'rule andLeft' 
836094     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [238] goal: 5666, source line: 328, command: 'rule andLeft' 
836094     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [239] goal: 5667, source line: 329, command: 'rule andLeft' 
836094     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [240] goal: 5668, source line: 330, command: 'rule ifthenelse_split occ=0' 
836095     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [241] goal: 5669, source line: 331, command: 'tryclose branch' 
836206     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [242] goal: 5670, source line: 332, command: 'tryclose branch' 
836213     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [243] goal: 5665, source line: 333, command: 'tryclose branch' 
836331     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [244] goal: 5661, source line: 334, command: 'rule getOfSwap' 
836332     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [245] goal: 5887, source line: 336, command: 'rule ifthenelse_negated' 
836333     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [246] goal: 5888, source line: 337, command: 'rule ifthenelse_split occ=0' 
836334     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [247] goal: 5889, source line: 338, command: 'rule andLeft' 
836335     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [248] goal: 5891, source line: 339, command: 'rule andLeft' 
836335     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [249] goal: 5892, source line: 340, command: 'rule andLeft' 
836336     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [250] goal: 5893, source line: 341, command: 'rule ifthenelse_split occ=0' 
836336     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [251] goal: 5894, source line: 342, command: 'tryclose branch' 
836343     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [252] goal: 5895, source line: 343, command: 'rule ifthenelse_split occ=0' 
836344     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [253] goal: 5897, source line: 344, command: 'tryclose branch' 
836446     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [254] goal: 5898, source line: 345, command: 'tryclose branch' 
836453     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [255] goal: 5890, source line: 346, command: 'tryclose branch' 
836459     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [256] goal: 5340, source line: 347, command: 'tryclose branch' 
836593     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [257] goal: 4954, source line: 348, command: 'rule getOfSwap' 
836594     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [258] goal: 6115, source line: 350, command: 'rule ifthenelse_negated' 
836595     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [259] goal: 6116, source line: 351, command: 'rule ifthenelse_split occ=0' 
836596     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [260] goal: 6117, source line: 352, command: 'rule andLeft' 
836597     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [261] goal: 6119, source line: 353, command: 'rule andLeft' 
836597     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [262] goal: 6120, source line: 354, command: 'rule andLeft' 
836598     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [263] goal: 6121, source line: 355, command: 'rule ifthenelse_split occ=0' 
836598     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [264] goal: 6122, source line: 356, command: 'tryclose branch' 
836670     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [265] goal: 6123, source line: 357, command: 'rule ifthenelse_split occ=0' 
836671     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [266] goal: 6193, source line: 358, command: 'rule getOfSwap' 
836672     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [267] goal: 6195, source line: 359, command: 'rule ifthenelse_negated' 
836672     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [268] goal: 6196, source line: 360, command: 'rule ifthenelse_split occ=0' 
836673     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [269] goal: 6197, source line: 361, command: 'tryclose branch' 
836680     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [270] goal: 6198, source line: 362, command: 'tryclose branch' 
836686     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [271] goal: 6194, source line: 363, command: 'tryclose branch' 
836836     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [272] goal: 6118, source line: 364, command: 'tryclose branch' 
836952     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [273] goal: 4952, source line: 365, command: 'rule getOfSwap' 
836952     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [274] goal: 6456, source line: 367, command: 'rule ifthenelse_negated' 
836953     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [275] goal: 6457, source line: 368, command: 'rule ifthenelse_split occ=0' 
836954     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [276] goal: 6458, source line: 369, command: 'tryclose branch' 
837170     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [277] goal: 6459, source line: 370, command: 'tryclose branch' 
837289     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'' 
837290     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [279] goal: 6735, source line: 375, command: 'tryclose branch' 
841115     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [280] goal: 6735, source line: 378, command: 'rule seqNPermSwapNPerm' 
841120     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [281] goal: 8783, source line: 380, command: 'instantiate hide var=iv with='jv_1'' 
841121     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'' 
841122     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [283] goal: 8785, source line: 382, command: 'rule impLeft' 
841123     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [284] goal: 8786, source line: 383, command: 'tryclose branch' 
841274     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))'' 
841274     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [286] goal: 8909, source line: 385, command: 'instantiate hide var=iv with='jv_1'' 
841276     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'' 
841277     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [288] goal: 8911, source line: 387, command: 'rule impLeft' 
841278     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [289] goal: 8912, source line: 388, command: 'tryclose branch' 
841415     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [290] goal: 8913, source line: 389, command: 'tryclose branch' 
845160     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [291] goal: 6736, source line: 390, command: 'tryclose branch' 
849223     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [292] goal: 6736, source line: 397, command: 'rule seqNPermSwapNPerm formula='seqNPerm(s_0)'' 
849228     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'' 
849229     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [294] goal: 12634, source line: 400, command: 'instantiate hide var=jv with='jv_0'' 
849231     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [295] goal: 12635, source line: 401, command: 'rule impLeft' 
849231     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [296] goal: 12636, source line: 402, command: 'tryclose branch' 
849379     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))'' 
849379     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'' 
849380     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [299] goal: 12758, source line: 405, command: 'instantiate hide var=jv with='jv_1'' 
849382     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)' ...' 
849382     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [301] goal: 12760, source line: 407, command: 'tryclose branch' 
850854     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm2/Taclet_schiffl_thm_1.proof 
850854     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 162.1ns 
850856     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
854228     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.37s 
854228     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: schiffl_thm_1 
855304     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: schiffl_thm_1 
855307     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 8.6ns 
855308     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [1] goal: 0, source line: 50, command: 'macro split-prop' 
855317     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)'' 
855330     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [3] goal: 11, source line: 52, command: 'instantiate hide var=x with='f_x'' 
855333     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [4] goal: 12, source line: 53, command: 'instantiate hide var=y with='f_y'' 
855336     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [5] goal: 13, source line: 54, command: 'rule impLeft' 
855338     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [6] goal: 14, source line: 55, command: 'tryclose branch' 
855343     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [7] goal: 15, source line: 56, command: 'rule exLeft' 
855344     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [8] goal: 23, source line: 57, command: 'macro split-prop' 
855349     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [9] goal: 27, source line: 58, command: 'rule seqPermDef occ=1' 
855351     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [10] goal: 28, source line: 59, command: 'rule andRight' 
855353     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [11] goal: 29, source line: 60, command: 'tryclose branch' 
855365     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [12] goal: 30, source line: 61, command: 'instantiate hide var=s with='r_0'' 
855366     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [13] goal: 46, source line: 62, command: 'rule andRight' 
855368     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [14] goal: 47, source line: 63, command: 'tryclose branch' 
855430     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [15] goal: 48, source line: 64, command: 'rule allRight' 
855431     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [16] goal: 119, source line: 65, command: 'rule impRight' 
855432     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [17] goal: 120, source line: 66, command: 'instantiate hide var=iv with='iv_0'' 
855433     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [18] goal: 121, source line: 67, command: 'rule impLeft' 
855434     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [19] goal: 122, source line: 68, command: 'tryclose branch' 
855519     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [20] goal: 123, source line: 69, command: 'rule andLeft' 
855520     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [21] goal: 203, source line: 70, command: 'rule seqNPermRange' 
855522     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [22] goal: 204, source line: 71, command: 'instantiate hide var=iv with='iv_0'' 
855523     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [23] goal: 205, source line: 72, command: 'rule impLeft' 
855524     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [24] goal: 206, source line: 73, command: 'tryclose branch' 
855529     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [25] goal: 207, source line: 74, command: 'rule andLeft' 
855529     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [26] goal: 215, source line: 75, command: 'rule andLeft' 
855530     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [27] goal: 216, source line: 76, command: 'rule seqNPermRange' 
855531     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [28] goal: 217, source line: 77, command: 'instantiate hide var=iv with='f_x'' 
855532     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [29] goal: 218, source line: 78, command: 'rule impLeft' 
855533     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [30] goal: 219, source line: 79, command: 'tryclose branch' 
855639     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [31] goal: 220, source line: 80, command: 'rule andLeft' 
855640     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [32] goal: 311, source line: 81, command: 'rule andLeft' 
855640     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [33] goal: 312, source line: 82, command: 'rule seqNPermRange' 
855641     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [34] goal: 313, source line: 83, command: 'instantiate hide var=iv with='f_y'' 
855643     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [35] goal: 314, source line: 84, command: 'rule impLeft' 
855644     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [36] goal: 315, source line: 85, command: 'tryclose branch' 
855759     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [37] goal: 316, source line: 86, command: 'rule andLeft' 
855760     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [38] goal: 410, source line: 87, command: 'rule andLeft' 
855761     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [39] goal: 411, source line: 88, command: 'rule getOfSeqDef occ=0' 
855761     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [40] goal: 412, source line: 89, command: 'rule getOfSeqDef' 
855762     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [41] goal: 413, source line: 90, command: 'rule ifthenelse_split occ=0' 
855763     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [42] goal: 414, source line: 91, command: 'rule andLeft occ=0' 
855764     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [43] goal: 416, source line: 92, command: 'rule sub_zero_2 occ=0' 
855765     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [44] goal: 417, source line: 93, command: 'rule ifthenelse_split occ=2' 
855766     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [45] goal: 418, source line: 94, command: 'rule andLeft' 
855766     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [46] goal: 420, source line: 95, command: 'rule sub_zero_2 occ=0' 
855767     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [47] goal: 421, source line: 96, command: 'rule add_zero_right occ=0' 
855767     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [48] goal: 422, source line: 97, command: 'rule add_zero_right occ=0' 
855768     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [49] goal: 423, source line: 98, command: 'rule add_zero_right occ=0' 
855769     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [50] goal: 424, source line: 99, command: 'rule add_zero_right occ=0' 
855769     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [51] goal: 425, source line: 100, command: 'rule add_zero_right occ=0' 
855770     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [52] goal: 426, source line: 101, command: 'rule add_zero_right occ=0' 
855771     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [53] goal: 427, source line: 102, command: 'rule ifthenelse_split occ=0' 
855771     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [54] goal: 428, source line: 103, command: 'rule ifthenelse_split occ=0' 
855772     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [55] goal: 430, source line: 104, command: 'tryclose branch' 
855776     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [56] goal: 431, source line: 105, command: 'tryclose branch' 
855826     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [57] goal: 429, source line: 106, command: 'rule ifthenelse_split occ=0' 
855827     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [58] goal: 473, source line: 107, command: 'tryclose branch' 
855906     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [59] goal: 474, source line: 108, command: 'rule ifthenelse_split occ=0' 
855907     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [60] goal: 541, source line: 109, command: 'rule seqNPermInjective' 
855908     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [61] goal: 543, source line: 110, command: 'instantiate hide var=iv with='iv_0'' 
855909     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [62] goal: 544, source line: 111, command: 'instantiate hide var=jv with='f_y'' 
855911     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [63] goal: 545, source line: 112, command: 'rule impLeft' 
855912     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [64] goal: 546, source line: 113, command: 'tryclose branch' 
855971     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [65] goal: 547, source line: 114, command: 'tryclose branch' 
855974     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [66] goal: 542, source line: 115, command: 'rule ifthenelse_split occ=0' 
855976     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [67] goal: 606, source line: 116, command: 'rule seqNPermInjective' 
855977     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [68] goal: 608, source line: 117, command: 'instantiate hide var=iv with='iv_0'' 
855978     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [69] goal: 609, source line: 118, command: 'instantiate hide var=jv with='f_x'' 
855980     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [70] goal: 610, source line: 119, command: 'rule impLeft' 
855981     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [71] goal: 611, source line: 120, command: 'tryclose branch' 
856049     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [72] goal: 612, source line: 121, command: 'tryclose branch' 
856052     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [73] goal: 607, source line: 122, command: 'tryclose branch' 
856056     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [74] goal: 419, source line: 123, command: 'tryclose branch' 
856124     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [75] goal: 415, source line: 124, command: 'tryclose branch' 
856193     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_eqSameSeq.proof 
856193     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 305.4ns 
856194     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
859330     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.14s 
859330     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: eqSameSeq 
860408     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: eqSameSeq 
860446     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 34.23ms