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

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

tests
0

failures
0

ignored
10m22.59s

duration
100%

successful

Tests

Test Method name Duration Result
powPositive data()[100] 3.012s passed
powPositiveConcrete data()[101] 3.006s passed
powGeq1Concrete data()[102] 3.024s passed
pow2InIntLower data()[103] 3.005s passed
pow2InIntUpper data()[104] 3.003s passed
logSelfConcrete data()[105] 3.020s passed
log1Concrete data()[106] 2.998s passed
logProduct data()[107] 3.003s passed
logTimesBaseConcrete data()[108] 3.030s passed
logProdIdentity data()[109] 3.039s passed
moduloByteIsInByte data()[10] 3.090s passed
logProdIdentityConcrete data()[110] 3.028s passed
logPowIdentity data()[111] 3.033s passed
logPowIdentityConcrete data()[112] 3.005s passed
logPositive data()[113] 3.007s passed
logPositiveConcrete data()[114] 3.024s passed
logMono data()[115] 3.022s passed
logMonoConcrete data()[116] 3.002s passed
powLogLess data()[117] 3.029s passed
powLogMore2 data()[118] 3.009s passed
logLessThanPow data()[119] 3.039s passed
moduloCharIsInChar data()[11] 3.059s passed
logLessThanPowConcrete data()[120] 3.021s passed
logSqueeze data()[121] 3.026s passed
ifthenelse_equals data()[122] 3.014s passed
ifthenelse_equals_1 data()[123] 3.021s passed
ifthenelse_equals_2 data()[124] 3.018s passed
disjointWithSingleton1 data()[125] 3.015s passed
disjointWithSingleton2 data()[126] 3.007s passed
disjointArrayRanges data()[127] 3.026s passed
disjointArrayRangeAllFields1 data()[128] 3.012s passed
disjointArrayRangeAllFields2 data()[129] 3.022s passed
div_unique1 data()[12] 3.145s passed
seqSelfDefinition data()[130] 3.022s passed
seqOutsideValue data()[131] 3.029s passed
castedGetAny data()[132] 3.006s passed
seqGetAlphaCast data()[133] 3.049s passed
getOfSeqSingleton data()[134] 3.036s passed
getOfSeqSingletonConcrete data()[135] 3.012s passed
getOfSeqConcat data()[136] 3.034s passed
getOfSeqSub data()[137] 3.015s passed
getOfSeqReverse data()[138] 3.031s passed
lenOfSeqEmpty data()[139] 3.027s passed
div_unique2 data()[13] 3.099s passed
lenOfSeqSingleton data()[140] 3.005s passed
lenOfSeqConcat data()[141] 3.032s passed
lenOfSeqSub data()[142] 3.019s passed
lenOfSeqReverse data()[143] 3.031s passed
equalityToSeqGetAndSeqLenLeft data()[144] 3.009s passed
equalityToSeqGetAndSeqLenRight data()[145] 3.025s passed
getOfSeqSingletonEQ data()[146] 3.028s passed
getOfSeqConcatEQ data()[147] 3.004s passed
getOfSeqSubEQ data()[148] 3.028s passed
getOfSeqReverseEQ data()[149] 3.029s passed
div_exists data()[14] 3.268s passed
lenOfSeqEmptyEQ data()[150] 3.032s passed
lenOfSeqSingletonEQ data()[151] 3.028s passed
lenOfSeqConcatEQ data()[152] 3.006s passed
lenOfSeqSubEQ data()[153] 3.025s passed
lenOfSeqReverseEQ data()[154] 3.022s passed
getOfSeqDefEQ data()[155] 3.021s passed
lenOfSeqDefEQ data()[156] 3.032s passed
seqConcatWithSeqEmpty1 data()[157] 3.033s passed
seqConcatWithSeqEmpty2 data()[158] 3.030s passed
seqReverseOfSeqEmpty data()[159] 3.024s passed
div_one data()[15] 3.088s passed
subSeqComplete data()[160] 3.040s passed
subSeqTailR data()[161] 3.033s passed
subSeqTailL data()[162] 3.025s passed
subSeqTailEQR data()[163] 3.028s passed
subSeqTailEQL data()[164] 3.034s passed
seqDef_split data()[165] 3.035s passed
seqDef_induction_upper data()[166] 3.041s passed
seqDef_induction_upper_concrete data()[167] 3.037s passed
seqDef_induction_lower data()[168] 3.045s passed
seqDef_induction_lower_concrete data()[169] 3.038s passed
jdiv_one data()[16] 3.045s passed
seqDef_split_in_three data()[170] 3.083s passed
seqDef_empty data()[171] 3.030s passed
seqDef_one_summand data()[172] 3.027s passed
seqDef_lower_equals_upper data()[173] 3.023s passed
seqDefOfSeq data()[174] 3.030s passed
seqSelfDefinitionEQ2 data()[175] 3.023s passed
indexOfSeqSingleton data()[176] 3.038s passed
indexOfSeqConcatFirst data()[177] 3.028s passed
indexOfSeqConcatSecond data()[178] 3.049s passed
indexOfSeqSub data()[179] 3.031s passed
div_zero data()[17] 3.121s passed
lenOfArray2seq data()[180] 3.019s passed
getAnyOfArray2seq data()[181] 3.017s passed
getOfArray2seq data()[182] 3.043s passed
getAnyOfNPermInv data()[183] 3.025s passed
seqNPermRange data()[184] 3.051s passed
seqPermTrans data()[185] 3.039s passed
seqPermRefl data()[186] 3.057s passed
seqPermSplit data()[187] 3.019s passed
seqNPermRight data()[188] 3.105s passed
seqPermFromSwap data()[189] 3.070s passed
divResZero1 data()[18] 3.083s passed
seqPermTransAlt0 data()[190] 3.024s passed
seqPermTransAlt1 data()[191] 3.032s passed
seqPermTransAlt2 data()[192] 3.016s passed
seqPermTransAlt3 data()[193] 3.016s passed
seqPermForall data()[194] 3.123s passed
seqPermExists data()[195] 3.082s passed
schiffl_lemma_2 data()[196] 20.855s passed
schiffl_thm_1 data()[197] 4.227s passed
eqSameSeq data()[198] 3.023s passed
divResZero2 data()[19] 3.066s passed
eqTermCut data()[1] 3.639s passed
divResOne1 data()[20] 3.090s passed
divResOne2 data()[21] 3.063s passed
div_cancel1 data()[22] 3.065s passed
div_cancel2 data()[23] 3.023s passed
divAddMultDenom data()[24] 3.082s passed
divMinus data()[25] 3.101s passed
divMinusDenom data()[26] 3.053s passed
divLeastDPos data()[27] 3.053s passed
divLeastDNeg data()[28] 3.037s passed
divGreatestDPos data()[29] 3.045s passed
equivAllRight data()[2] 3.363s passed
divGreatestDNeg data()[30] 3.018s passed
divIncreasingPos data()[31] 3.037s passed
divIncreasingNeg data()[32] 3.035s passed
jdiv_zero data()[33] 3.037s passed
jdivPulloutMinusNum data()[34] 3.054s passed
jdivPulloutMinusDenom data()[35] 3.061s passed
jdiv_uniquePosPos data()[36] 3.050s passed
jdiv_uniquePosNeg data()[37] 3.055s passed
jdiv_uniqueNegPos data()[38] 3.043s passed
jdiv_uniqueNegNeg data()[39] 3.036s passed
irrflConcrete1 data()[3] 3.349s passed
jdivMultDenom1 data()[40] 3.095s passed
jdivMultDenom2 data()[41] 3.055s passed
mod_geZero data()[42] 3.101s passed
mod_lessDenom data()[43] 3.046s passed
jmod_NumPos data()[44] 3.027s passed
jmod_NumNeg data()[45] 3.041s passed
jmod_geZero data()[46] 3.046s passed
jmodNumZero data()[47] 3.016s passed
jmod_pulloutminusNum data()[48] 3.011s passed
jmod_pulloutminusDenom data()[49] 3.034s passed
irrflConcrete2 data()[4] 3.171s passed
jmodUnique1 data()[50] 3.092s passed
jmodUnique2 data()[51] 3.063s passed
intDivRem data()[52] 3.022s passed
jmodjmod data()[53] 3.052s passed
jmodDivisible data()[54] 3.022s passed
jmodDivisibleRep data()[55] 3.035s passed
jdivAddMultDenom data()[56] 3.127s passed
jmodAltZero data()[57] 3.040s passed
jmodAddMultDenomZero data()[58] 3.036s passed
polyDiv_zero data()[59] 3.017s passed
cancel_gtPos data()[5] 3.232s passed
polyMod_ltdivDenom data()[60] 3.016s passed
bsum_empty data()[61] 3.003s passed
bsum_induction_upper data()[62] 3.022s passed
bsum_induction_lower data()[63] 3.011s passed
bsum_num_of_bounds data()[64] 3.015s passed
bsum_num_of_bounds2 data()[65] 3.033s passed
bsum_induction_upper2 data()[66] 3.029s passed
bsum_induction_upper_concrete data()[67] 3.128s passed
bsum_induction_upper_concrete_2 data()[68] 3.146s passed
bsum_induction_upper2_concrete data()[69] 3.080s passed
cancel_gtNeg data()[6] 3.214s passed
bsum_induction_lower_concrete data()[70] 3.015s passed
bsum_induction_lower2 data()[71] 3.022s passed
bsum_induction_lower2_concrete data()[72] 3.011s passed
bsum_positive data()[73] 3.036s passed
bsum_upper_bound data()[74] 3.064s passed
bsum_lower_bound data()[75] 3.030s passed
bsum_positive_lower_bound_element data()[76] 3.048s passed
bsum_sub_same_index data()[77] 3.043s passed
bsum_less_same_index data()[78] 3.047s passed
bsum_equal_except_one_index data()[79] 3.048s passed
moduloIntIsInInt data()[7] 3.196s passed
bsum_num_of_is_max data()[80] 3.032s passed
bsum_num_of_is_max2 data()[81] 3.028s passed
bsum_num_of_is_max3 data()[82] 3.019s passed
bsum_num_of_is_max4 data()[83] 3.039s passed
bsum_num_of_lt_max data()[84] 3.019s passed
bsum_num_of_lt_max2 data()[85] 3.020s passed
bsum_num_of_lt_max3 data()[86] 3.050s passed
bsum_num_of_lt_max4 data()[87] 3.013s passed
bsum_num_of_gt0 data()[88] 3.021s passed
bsum_num_of_gt0_alt data()[89] 3.014s passed
moduloLongIsInLong data()[8] 3.114s passed
bsum_add_concrete data()[90] 3.027s passed
bprod_all_positive data()[91] 3.014s passed
bprod_split data()[92] 3.014s passed
powConcrete0 data()[93] 3.021s passed
powConcrete1 data()[94] 3.013s passed
powSplitFactor data()[95] 2.999s passed
powAdd data()[96] 3.051s passed
powMono data()[97] 3.015s passed
powMonoConcrete data()[98] 3.013s passed
powMonoConcreteRight data()[99] 3.023s passed
moduloShortIsInShort data()[9] 3.134s passed

Standard output

307        INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src/test/resources/testcase/dummyTrue.key 
334        DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 10.85ms 
553        INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
565        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)

1534       DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for Meta 
1540       DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for Meta 
1544       DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for Meta 
1545       DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for Meta 
2801       DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for JavaBigintExpression 
7593       DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 7.04s 
7648       INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof dummyTrue.key 
7678       DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 33.3ns 
7692       INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/firstOrder/Taclet_eqTermCut.proof 
7692       DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 545.2ns 
7726       INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
10374      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.65s 
10376      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: eqTermCut 
11300      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: eqTermCut 
11322      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 16.75ms 
11331      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/firstOrder/Taclet_equivAllRight.proof 
11331      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 130ns 
11332      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
13877      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.55s 
13877      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: equivAllRight 
14679      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: equivAllRight 
14692      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 9.06ms 
14695      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_irrflConcrete1.proof 
14695      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 356.3ns 
14697      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
17199      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.5s 
17200      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: irrflConcrete1 
18036      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: irrflConcrete1 
18042      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.63ms 
18045      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_irrflConcrete2.proof 
18045      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 137.2ns 
18046      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
20420      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.37s 
20420      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: irrflConcrete2 
21210      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: irrflConcrete2 
21215      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.25ms 
21216      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_cancel_gtPos.proof 
21216      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 117.2ns 
21217      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
23584      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.37s 
23584      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: cancel_gtPos 
24380      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: cancel_gtPos 
24446      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 61.98ms 
24452      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_cancel_gtNeg.proof 
24453      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 528.5ns 
24454      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
26827      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.37s 
26827      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: cancel_gtNeg 
27647      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: cancel_gtNeg 
27663      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 13.63ms 
27667      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intRulesIgnoringOF/Taclet_moduloIntIsInInt.proof 
27667      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 351.7ns 
27668      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
30032      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.36s 
30033      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: moduloIntIsInInt 
30857      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: moduloIntIsInInt 
30860      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 637.6ns 
30863      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intRulesIgnoringOF/Taclet_moduloLongIsInLong.proof 
30863      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 312.4ns 
30864      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
33225      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.36s 
33226      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: moduloLongIsInLong 
33972      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: moduloLongIsInLong 
33975      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 574ns 
33977      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intRulesIgnoringOF/Taclet_moduloShortIsInShort.proof 
33978      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 312.8ns 
33979      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
36320      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.34s 
36321      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: moduloShortIsInShort 
37103      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: moduloShortIsInShort 
37108      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.57ms 
37111      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intRulesIgnoringOF/Taclet_moduloByteIsInByte.proof 
37112      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 372.4ns 
37113      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
39438      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.33s 
39439      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: moduloByteIsInByte 
40198      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: moduloByteIsInByte 
40201      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 518.9ns 
40202      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intRulesIgnoringOF/Taclet_moduloCharIsInChar.proof 
40202      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 97.9ns 
40203      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
42519      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.32s 
42519      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: moduloCharIsInChar 
43257      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: moduloCharIsInChar 
43259      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 608.5ns 
43261      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_div_unique1.proof 
43261      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 110ns 
43262      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
45598      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.34s 
45599      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: div_unique1 
46357      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: div_unique1 
46404      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 42.92ms 
46406      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_div_unique2.proof 
46406      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 127.8ns 
46407      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
48711      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.3s 
48712      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: div_unique2 
49468      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: div_unique2 
49503      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 31.61ms 
49505      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_div_exists.proof 
49505      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 136.1ns 
49507      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
51825      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.32s 
51826      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: div_exists 
52577      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: div_exists 
52771      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 184.33ms 
52776      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_div_one.proof 
52777      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 537.9ns 
52778      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
55087      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.31s 
55087      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: div_one 
55856      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: div_one 
55861      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.63ms 
55863      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdiv_one.proof 
55863      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 374ns 
55864      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
58150      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.29s 
58151      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdiv_one 
58903      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdiv_one 
58906      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.19ms 
58909      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_div_zero.proof 
58910      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 303.2ns 
58911      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
61229      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.32s 
61231      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: div_zero 
61975      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: div_zero 
62027      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 47.75ms 
62031      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divResZero1.proof 
62031      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 324.4ns 
62032      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
64345      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.31s 
64346      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divResZero1 
65100      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divResZero1 
65112      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 9.45ms 
65114      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divResZero2.proof 
65114      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 94.4ns 
65115      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
67402      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.29s 
67403      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divResZero2 
68166      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divResZero2 
68179      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 10.25ms 
68180      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divResOne1.proof 
68180      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 110.7ns 
68185      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
70490      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.31s 
70490      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divResOne1 
71255      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divResOne1 
71268      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 9.59ms 
71270      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divResOne2.proof 
71270      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 314.2ns 
71271      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
73567      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.3s 
73567      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divResOne2 
74318      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divResOne2 
74331      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 9.17ms 
74333      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_div_cancel1.proof 
74333      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 314ns 
74334      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
76626      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.29s 
76626      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: div_cancel1 
77379      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: div_cancel1 
77396      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 14.13ms 
77398      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_div_cancel2.proof 
77398      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 114.6ns 
77399      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
79667      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.27s 
79667      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: div_cancel2 
80416      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: div_cancel2 
80419      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.33ms 
80420      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divAddMultDenom.proof 
80420      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 98.9ns 
80421      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
82710      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.29s 
82710      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divAddMultDenom 
83470      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divAddMultDenom 
83501      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 25.97ms 
83503      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divMinus.proof 
83503      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 112.2ns 
83504      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
85800      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.3s 
85801      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divMinus 
86557      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divMinus 
86601      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 37.5ms 
86604      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divMinusDenom.proof 
86606      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 1ms 
86607      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
88879      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.27s 
88879      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divMinusDenom 
89626      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divMinusDenom 
89656      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 24.66ms 
89658      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divLeastDPos.proof 
89658      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 101ns 
89658      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
91946      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.29s 
91947      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divLeastDPos 
92698      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divLeastDPos 
92709      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 9.03ms 
92710      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divLeastDNeg.proof 
92710      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 88ns 
92711      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
94985      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.27s 
94986      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divLeastDNeg 
95736      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divLeastDNeg 
95747      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 8.56ms 
95748      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divGreatestDPos.proof 
95748      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 96.4ns 
95749      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
98014      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.27s 
98014      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divGreatestDPos 
98781      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divGreatestDPos 
98791      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 7.14ms 
98792      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divGreatestDNeg.proof 
98792      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 87.2ns 
98793      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
101077     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.28s 
101077     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divGreatestDNeg 
101804     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divGreatestDNeg 
101810     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.31ms 
101811     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divIncreasingPos.proof 
101811     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 90.6ns 
101812     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
104093     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.28s 
104093     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divIncreasingPos 
104840     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divIncreasingPos 
104846     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.06ms 
104848     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divIncreasingNeg.proof 
104848     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 230.9ns 
104849     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
107128     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.28s 
107128     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divIncreasingNeg 
107875     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divIncreasingNeg 
107881     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.85ms 
107882     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdiv_zero.proof 
107882     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 149.7ns 
107883     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
110178     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.29s 
110178     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdiv_zero 
110915     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdiv_zero 
110919     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.38ms 
110920     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdivPulloutMinusNum.proof 
110920     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 146.8ns 
110921     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
113218     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.3s 
113218     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdivPulloutMinusNum 
113963     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdivPulloutMinusNum 
113972     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 6.4ms 
113973     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdivPulloutMinusDenom.proof 
113973     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 92.1ns 
113974     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
116238     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.26s 
116238     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdivPulloutMinusDenom 
116985     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdivPulloutMinusDenom 
117031     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 36.11ms 
117036     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdiv_uniquePosPos.proof 
117036     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 107.1ns 
117037     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
119333     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.3s 
119333     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdiv_uniquePosPos 
120062     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdiv_uniquePosPos 
120084     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 14.3ms 
120087     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdiv_uniquePosNeg.proof 
120087     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 278.4ns 
120089     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
122375     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.29s 
122375     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdiv_uniquePosNeg 
123123     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdiv_uniquePosNeg 
123140     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 14.55ms 
123143     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdiv_uniqueNegPos.proof 
123143     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 318.8ns 
123144     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
125423     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.28s 
125424     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdiv_uniqueNegPos 
126169     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdiv_uniqueNegPos 
126183     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 9.87ms 
126185     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdiv_uniqueNegNeg.proof 
126185     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 251.9ns 
126186     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
128475     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.29s 
128475     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdiv_uniqueNegNeg 
129207     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdiv_uniqueNegNeg 
129219     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 9.18ms 
129220     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdivMultDenom1.proof 
129221     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 95.4ns 
129221     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
131540     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.32s 
131540     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdivMultDenom1 
132286     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdivMultDenom1 
132314     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 21.97ms 
132316     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdivMultDenom2.proof 
132316     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 276.5ns 
132317     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
134591     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.27s 
134591     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdivMultDenom2 
135367     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdivMultDenom2 
135370     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 847ns 
135371     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_mod_geZero.proof 
135371     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 140.6ns 
135372     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
137719     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.35s 
137719     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: mod_geZero 
138461     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: mod_geZero 
138470     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.59ms 
138472     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_mod_lessDenom.proof 
138472     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 82.6ns 
138473     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
140762     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.29s 
140762     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: mod_lessDenom 
141511     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: mod_lessDenom 
141517     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.07ms 
141519     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmod_NumPos.proof 
141519     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 75.8ns 
141519     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
143791     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.27s 
143791     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmod_NumPos 
144538     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmod_NumPos 
144544     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.07ms 
144545     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmod_NumNeg.proof 
144546     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 84.5ns 
144547     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
146813     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.27s 
146813     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmod_NumNeg 
147561     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmod_NumNeg 
147585     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 21.16ms 
147588     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmod_geZero.proof 
147588     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 277.4ns 
147589     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
149878     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.29s 
149878     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmod_geZero 
150625     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmod_geZero 
150631     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.12ms 
150632     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmodNumZero.proof 
150632     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 77.8ns 
150633     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
152897     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.26s 
152898     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmodNumZero 
153644     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmodNumZero 
153647     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 883.1ns 
153649     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmod_pulloutminusNum.proof 
153649     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 240.8ns 
153650     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
155909     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.26s 
155909     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmod_pulloutminusNum 
156655     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmod_pulloutminusNum 
156658     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.08ms 
156659     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmod_pulloutminusDenom.proof 
156659     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 79.7ns 
156660     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
158936     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.28s 
158936     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmod_pulloutminusDenom 
159681     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmod_pulloutminusDenom 
159690     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 7.28ms 
159704     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmodUnique1.proof 
159704     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 106.1ns 
159705     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
161989     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.28s 
161989     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmodUnique1 
162737     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmodUnique1 
162785     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 39.18ms 
162786     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmodUnique2.proof 
162786     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 85.6ns 
162787     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
165047     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.26s 
165047     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmodUnique2 
165791     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmodUnique2 
165848     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 47.71ms 
165849     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_intDivRem.proof 
165849     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 84.6ns 
165850     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
168125     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.27s 
168125     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: intDivRem 
168868     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: intDivRem 
168871     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.09ms 
168872     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmodjmod.proof 
168872     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 134.3ns 
168873     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
171150     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.28s 
171151     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmodjmod 
171896     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmodjmod 
171922     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 21.66ms 
171924     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmodDivisible.proof 
171924     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 209.2ns 
171925     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
174182     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.26s 
174182     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmodDivisible 
174927     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmodDivisible 
174945     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 14.89ms 
174946     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmodDivisibleRep.proof 
174946     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 93.5ns 
174947     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
177221     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.27s 
177221     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmodDivisibleRep 
177970     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmodDivisibleRep 
177973     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 867.6ns 
177988     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdivAddMultDenom.proof 
177989     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 284.7ns 
177990     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
180255     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.27s 
180255     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdivAddMultDenom 
181007     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdivAddMultDenom 
181113     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 94.19ms 
181114     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmodAltZero.proof 
181115     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 82.2ns 
181121     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
183404     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.28s 
183404     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmodAltZero 
184147     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmodAltZero 
184154     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 5.26ms 
184155     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmodAddMultDenomZero.proof 
184155     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 62.9ns 
184156     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
186439     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.28s 
186440     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmodAddMultDenomZero 
187184     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmodAddMultDenomZero 
187190     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.38ms 
187191     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_polyDiv_zero.proof 
187191     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 67ns 
187191     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
189450     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.26s 
189450     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: polyDiv_zero 
190195     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: polyDiv_zero 
190207     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 9.33ms 
190208     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_polyMod_ltdivDenom.proof 
190208     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 70.4ns 
190209     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
192468     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.26s 
192468     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: polyMod_ltdivDenom 
193213     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: polyMod_ltdivDenom 
193222     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.6ms 
193225     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_empty.proof 
193226     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 1.3ms 
193227     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
195497     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.27s 
195497     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_empty 
196222     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_empty 
196225     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.19ms 
196226     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_induction_upper.proof 
196226     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 55.8ns 
196227     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
198499     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.27s 
198499     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_upper 
199244     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_induction_upper 
199248     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.84ms 
199249     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_induction_lower.proof 
199249     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 58.7ns 
199250     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
201503     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.25s 
201504     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_lower 
202246     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_induction_lower 
202258     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 9.56ms 
202260     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_bounds.proof 
202260     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 69.1ns 
202260     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
204538     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.28s 
204538     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_bounds 
205263     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_bounds 
205273     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 7.98ms 
205274     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_bounds2.proof 
205274     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 67.7ns 
205275     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
207546     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.27s 
207546     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_bounds2 
208294     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_bounds2 
208306     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 9.72ms 
208307     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_induction_upper2.proof 
208307     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 101.1ns 
208308     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
210566     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.26s 
210567     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_upper2 
211333     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_induction_upper2 
211335     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 756.5ns 
211336     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_induction_upper_concrete.proof 
211336     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 54.5ns 
211337     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
213710     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.37s 
213711     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_upper_concrete 
214461     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_induction_upper_concrete 
214464     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.16ms 
214465     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_induction_upper_concrete_2.proof 
214465     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 119.8ns 
214466     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
216833     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.37s 
216833     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_upper_concrete_2 
217606     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_induction_upper_concrete_2 
217610     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.21ms 
217611     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_induction_upper2_concrete.proof 
217611     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 59.8ns 
217611     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
219936     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.32s 
219936     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_upper2_concrete 
220686     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_induction_upper2_concrete 
220689     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 747.3ns 
220690     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_induction_lower_concrete.proof 
220691     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 191.8ns 
220691     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
222981     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.29s 
222981     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_lower_concrete 
223702     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_induction_lower_concrete 
223704     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 413.1ns 
223705     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_induction_lower2.proof 
223705     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 55.5ns 
223706     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
225982     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.28s 
225982     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_lower2 
226724     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_induction_lower2 
226727     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.33ms 
226728     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_induction_lower2_concrete.proof 
226728     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 84.7ns 
226729     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
228990     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.26s 
228991     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_lower2_concrete 
229735     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_induction_lower2_concrete 
229737     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 617.6ns 
229738     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_positive.proof 
229738     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 59.2ns 
229739     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
231990     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.25s 
231990     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_positive 
232732     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_positive 
232773     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 38.04ms 
232774     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_upper_bound.proof 
232774     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 72.7ns 
232775     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
235060     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.28s 
235060     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_upper_bound 
235807     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_upper_bound 
235837     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 27.14ms 
235839     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_lower_bound.proof 
235839     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 70.7ns 
235840     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
238101     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.26s 
238101     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_lower_bound 
238843     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_lower_bound 
238867     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 20.77ms 
238868     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_positive_lower_bound_element.proof 
238868     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 60.7ns 
238869     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
241129     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.26s 
241129     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_positive_lower_bound_element 
241883     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_positive_lower_bound_element 
241915     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 27.47ms 
241916     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_sub_same_index.proof 
241916     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 74.2ns 
241917     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
244194     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.28s 
244194     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_sub_same_index 
244938     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_sub_same_index 
244958     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 16.96ms 
244959     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_less_same_index.proof 
244959     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 70.8ns 
244960     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
247224     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.26s 
247224     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_less_same_index 
247966     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_less_same_index 
248005     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 34.83ms 
248006     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_equal_except_one_index.proof 
248006     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 65.3ns 
248007     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
250290     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.28s 
250290     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_equal_except_one_index 
251036     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_equal_except_one_index 
251053     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 14.66ms 
251055     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_is_max.proof 
251055     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 70.9ns 
251055     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
253328     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.27s 
253329     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_is_max 
254073     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_is_max 
254085     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 9.26ms 
254086     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_is_max2.proof 
254086     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 68.7ns 
254087     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
256353     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.27s 
256353     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_is_max2 
257099     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_is_max2 
257113     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 11.65ms 
257116     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_is_max3.proof 
257116     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 189.8ns 
257117     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
259376     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.26s 
259377     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_is_max3 
260120     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_is_max3 
260132     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 9.88ms 
260134     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_is_max4.proof 
260134     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 66.3ns 
260134     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
262411     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.28s 
262411     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_is_max4 
263155     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_is_max4 
263171     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 12.38ms 
263173     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_lt_max.proof 
263173     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 187ns 
263174     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
265432     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.26s 
265432     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_lt_max 
266175     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_lt_max 
266190     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 12.02ms 
266192     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_lt_max2.proof 
266192     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 76.6ns 
266192     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
268451     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.26s 
268452     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_lt_max2 
269195     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_lt_max2 
269210     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 12.14ms 
269212     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_lt_max3.proof 
269212     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 68.9ns 
269213     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
271495     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.28s 
271495     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_lt_max3 
272220     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_lt_max3 
272260     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 11.3ms 
272262     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_lt_max4.proof 
272262     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 221.1ns 
272263     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
274516     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.25s 
274516     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_lt_max4 
275260     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_lt_max4 
275273     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 10.35ms 
275274     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_gt0.proof 
275274     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 64ns 
275275     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
277532     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.26s 
277533     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_gt0 
278279     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_gt0 
278294     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 11.91ms 
278295     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_gt0_alt.proof 
278295     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 86.8ns 
278296     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
280570     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.27s 
280570     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_gt0_alt 
281293     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_gt0_alt 
281308     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 12.36ms 
281310     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_add_concrete.proof 
281310     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 75.1ns 
281310     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
283586     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.28s 
283587     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_add_concrete 
284330     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_add_concrete 
284336     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.43ms 
284337     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bprod/Taclet_bprod_all_positive.proof 
284337     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 54.1ns 
284337     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
286596     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.26s 
286597     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bprod_all_positive 
287339     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bprod_all_positive 
287349     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 8.12ms 
287350     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bprod/Taclet_bprod_split.proof 
287350     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 49.1ns 
287351     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
289636     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.28s 
289636     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bprod_split 
290360     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bprod_split 
290363     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.54ms 
290364     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powConcrete0.proof 
290365     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 59.3ns 
290365     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
292638     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.27s 
292639     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powConcrete0 
293383     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powConcrete0 
293385     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 504.2ns 
293386     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powConcrete1.proof 
293386     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 60.3ns 
293387     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
295651     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.26s 
295652     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powConcrete1 
296395     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powConcrete1 
296397     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 576.5ns 
296398     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powSplitFactor.proof 
296398     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 49.8ns 
296399     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
298668     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.27s 
298668     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powSplitFactor 
299392     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powSplitFactor 
299397     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.71ms 
299398     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powAdd.proof 
299398     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 55.5ns 
299398     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
301698     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.3s 
301699     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powAdd 
302442     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powAdd 
302447     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.73ms 
302449     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powMono.proof 
302449     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 171.7ns 
302450     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
304710     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.26s 
304710     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powMono 
305453     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powMono 
305462     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 7.01ms 
305463     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powMonoConcrete.proof 
305463     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 59.1ns 
305464     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
307749     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.29s 
307750     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powMonoConcrete 
308472     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powMonoConcrete 
308475     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.45ms 
308477     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powMonoConcreteRight.proof 
308477     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 47.1ns 
308477     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
310753     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.28s 
310754     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powMonoConcreteRight 
311496     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powMonoConcreteRight 
311498     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 378.3ns 
311499     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powPositive.proof 
311499     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 59.1ns 
311500     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
313762     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.26s 
313762     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powPositive 
314506     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powPositive 
314511     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.38ms 
314512     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powPositiveConcrete.proof 
314512     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 60.2ns 
314512     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
316791     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.28s 
316791     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powPositiveConcrete 
317515     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powPositiveConcrete 
317517     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 458.9ns 
317518     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powGeq1Concrete.proof 
317518     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 48.1ns 
317518     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
319790     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.27s 
319790     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powGeq1Concrete 
320539     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powGeq1Concrete 
320541     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 466.2ns 
320542     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_pow2InIntLower.proof 
320542     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 59.4ns 
320542     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
322799     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.26s 
322800     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: pow2InIntLower 
323543     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: pow2InIntLower 
323545     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 432.9ns 
323546     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_pow2InIntUpper.proof 
323546     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 55.3ns 
323547     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
325800     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.25s 
325800     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: pow2InIntUpper 
326545     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: pow2InIntUpper 
326549     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.58ms 
326550     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logSelfConcrete.proof 
326550     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 58.6ns 
326550     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
328819     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.27s 
328819     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logSelfConcrete 
329561     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logSelfConcrete 
329568     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.74ms 
329569     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_log1Concrete.proof 
329569     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 47.3ns 
329570     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
331821     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.25s 
331821     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: log1Concrete 
332564     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: log1Concrete 
332567     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.41ms 
332568     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logProduct.proof 
332568     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 56.3ns 
332569     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
334819     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.25s 
334819     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logProduct 
335565     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logProduct 
335571     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.23ms 
335572     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logTimesBaseConcrete.proof 
335572     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 55.5ns 
335572     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
337855     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.28s 
337855     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logTimesBaseConcrete 
338597     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logTimesBaseConcrete 
338600     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.78ms 
338601     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logProdIdentity.proof 
338601     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 52.8ns 
338602     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
340870     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.27s 
340870     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logProdIdentity 
341628     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logProdIdentity 
341640     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 8.86ms 
341641     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logProdIdentityConcrete.proof 
341641     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 68.3ns 
341642     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
343922     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.28s 
343922     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logProdIdentityConcrete 
344664     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logProdIdentityConcrete 
344667     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.3ms 
344669     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logPowIdentity.proof 
344669     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 51.2ns 
344670     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
346952     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.28s 
346952     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logPowIdentity 
347698     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logPowIdentity 
347701     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 880.4ns 
347702     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logPowIdentityConcrete.proof 
347702     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 45.5ns 
347702     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
349959     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.26s 
349960     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logPowIdentityConcrete 
350702     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logPowIdentityConcrete 
350705     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.47ms 
350706     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logPositive.proof 
350706     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 46.4ns 
350707     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
352978     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.27s 
352979     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logPositive 
353700     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logPositive 
353712     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 9.48ms 
353713     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logPositiveConcrete.proof 
353713     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 59.4ns 
353714     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
355991     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.28s 
355991     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logPositiveConcrete 
356732     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logPositiveConcrete 
356736     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 278ns 
356737     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logMono.proof 
356737     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 59.4ns 
356738     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
358996     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.26s 
358996     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logMono 
359734     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logMono 
359759     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 20.55ms 
359760     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logMonoConcrete.proof 
359760     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 67.9ns 
359761     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
362035     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.27s 
362035     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logMonoConcrete 
362758     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logMonoConcrete 
362761     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.34ms 
362762     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powLogLess.proof 
362762     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 47.4ns 
362763     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
365031     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.27s 
365031     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powLogLess 
365775     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powLogLess 
365790     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 11.47ms 
365791     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powLogMore2.proof 
365791     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 57.7ns 
365792     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
368061     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.27s 
368061     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powLogMore2 
368785     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powLogMore2 
368798     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 10.88ms 
368799     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logLessThanPow.proof 
368799     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 62.5ns 
368800     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
371079     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.28s 
371080     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logLessThanPow 
371820     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logLessThanPow 
371837     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 13.63ms 
371838     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logLessThanPowConcrete.proof 
371838     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 75.4ns 
371839     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
374114     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.27s 
374114     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logLessThanPowConcrete 
374857     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logLessThanPowConcrete 
374859     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 420.3ns 
374860     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logSqueeze.proof 
374860     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 47ns 
374860     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
377133     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.27s 
377134     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logSqueeze 
377880     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logSqueeze 
377885     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.83ms 
377886     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/booleanRules/Taclet_ifthenelse_equals.proof 
377886     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 47.1ns 
377886     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
380150     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.26s 
380150     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: ifthenelse_equals 
380896     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: ifthenelse_equals 
380898     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.28ms 
380900     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/booleanRules/Taclet_ifthenelse_equals_1.proof 
380900     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 53.6ns 
380900     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
383170     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.27s 
383170     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: ifthenelse_equals_1 
383917     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: ifthenelse_equals_1 
383919     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 686.2ns 
383921     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/booleanRules/Taclet_ifthenelse_equals_2.proof 
383921     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 166.9ns 
383923     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
386187     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.26s 
386187     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: ifthenelse_equals_2 
386935     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: ifthenelse_equals_2 
386937     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 633.5ns 
386938     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/locSet/Taclet_disjointWithSingleton1.proof 
386938     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 51ns 
386939     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
389205     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.27s 
389205     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: disjointWithSingleton1 
389950     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: disjointWithSingleton1 
389952     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 983.1ns 
389953     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/locSet/Taclet_disjointWithSingleton2.proof 
389953     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 45.1ns 
389954     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
392211     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.26s 
392211     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: disjointWithSingleton2 
392957     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: disjointWithSingleton2 
392959     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 946.3ns 
392960     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/locSet/Taclet_disjointArrayRanges.proof 
392960     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 51.5ns 
392961     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
395232     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.27s 
395232     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: disjointArrayRanges 
395978     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: disjointArrayRanges 
395985     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 5.14ms 
395986     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/locSet/Taclet_disjointArrayRangeAllFields1.proof 
395987     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 59.4ns 
395987     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
398245     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.26s 
398245     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: disjointArrayRangeAllFields1 
398992     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: disjointArrayRangeAllFields1 
398998     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.99ms 
398999     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/locSet/Taclet_disjointArrayRangeAllFields2.proof 
398999     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 50.1ns 
398999     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
401268     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.27s 
401268     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: disjointArrayRangeAllFields2 
402014     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: disjointArrayRangeAllFields2 
402020     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.94ms 
402021     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqSelfDefinition.proof 
402021     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 53.8ns 
402021     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
404282     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.26s 
404282     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqSelfDefinition 
405035     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqSelfDefinition 
405041     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.59ms 
405042     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqOutsideValue.proof 
405043     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 79ns 
405043     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
407314     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.27s 
407314     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqOutsideValue 
408067     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqOutsideValue 
408071     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.94ms 
408073     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_castedGetAny.proof 
408074     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 190.6ns 
408074     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
410341     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.27s 
410341     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: castedGetAny 
411073     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: castedGetAny 
411077     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.13ms 
411078     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqGetAlphaCast.proof 
411078     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 46.5ns 
411079     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
413372     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.29s 
413372     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqGetAlphaCast 
414124     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqGetAlphaCast 
414126     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 619ns 
414127     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqSingleton.proof 
414127     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 54ns 
414128     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
416406     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.28s 
416407     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqSingleton 
417159     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqSingleton 
417161     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 798.7ns 
417163     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqSingletonConcrete.proof 
417163     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 184.2ns 
417164     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
419419     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.25s 
419419     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqSingletonConcrete 
420171     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqSingletonConcrete 
420173     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 810ns 
420174     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqConcat.proof 
420174     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 57.5ns 
420175     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
422448     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.27s 
422448     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqConcat 
423199     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqConcat 
423207     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 6.27ms 
423208     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqSub.proof 
423209     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 58.8ns 
423209     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
425486     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.28s 
425486     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqSub 
426220     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqSub 
426222     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.22ms 
426224     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqReverse.proof 
426224     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 59.2ns 
426224     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
428495     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.27s 
428495     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqReverse 
429249     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqReverse 
429254     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.29ms 
429255     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqEmpty.proof 
429255     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 60.5ns 
429255     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
431528     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.27s 
431528     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqEmpty 
432279     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqEmpty 
432281     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 689.3ns 
432282     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqSingleton.proof 
432282     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 52.6ns 
432282     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
434551     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.27s 
434551     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqSingleton 
435283     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqSingleton 
435285     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 520.1ns 
435286     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqConcat.proof 
435286     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 58.4ns 
435287     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
437561     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.27s 
437562     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqConcat 
438314     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqConcat 
438317     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.23ms 
438319     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqSub.proof 
438319     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 219.2ns 
438320     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
440584     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.26s 
440584     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqSub 
441334     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqSub 
441336     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 780.9ns 
441338     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqReverse.proof 
441338     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 46.1ns 
441338     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
443607     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.27s 
443607     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqReverse 
444365     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqReverse 
444367     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 945.5ns 
444368     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_equalityToSeqGetAndSeqLenLeft.proof 
444368     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 56.1ns 
444369     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
446623     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.25s 
446623     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: equalityToSeqGetAndSeqLenLeft 
447374     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: equalityToSeqGetAndSeqLenLeft 
447376     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 909.2ns 
447377     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_equalityToSeqGetAndSeqLenRight.proof 
447377     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 57.7ns 
447378     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
449645     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.27s 
449646     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: equalityToSeqGetAndSeqLenRight 
450398     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: equalityToSeqGetAndSeqLenRight 
450401     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.89ms 
450402     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqSingletonEQ.proof 
450402     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 56.1ns 
450403     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
452676     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.27s 
452677     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqSingletonEQ 
453427     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqSingletonEQ 
453430     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 844.2ns 
453431     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqConcatEQ.proof 
453431     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 45.8ns 
453431     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
455695     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.26s 
455695     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqConcatEQ 
456426     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqConcatEQ 
456434     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 5.63ms 
456435     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqSubEQ.proof 
456435     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 58ns 
456436     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
458709     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.27s 
458709     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqSubEQ 
459460     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqSubEQ 
459461     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 523.9ns 
459463     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqReverseEQ.proof 
459463     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 47ns 
459463     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
461733     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.27s 
461733     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqReverseEQ 
462485     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqReverseEQ 
462490     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.37ms 
462491     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqEmptyEQ.proof 
462491     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 54.1ns 
462492     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
464767     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.27s 
464767     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqEmptyEQ 
465519     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqEmptyEQ 
465522     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 774.5ns 
465524     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqSingletonEQ.proof 
465524     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 58.7ns 
465524     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
467796     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.27s 
467796     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqSingletonEQ 
468548     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqSingletonEQ 
468550     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 584.3ns 
468551     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqConcatEQ.proof 
468551     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 57.5ns 
468552     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
470819     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.27s 
470819     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqConcatEQ 
471553     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqConcatEQ 
471557     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.7ms 
471558     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqSubEQ.proof 
471558     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 44.1ns 
471558     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
473827     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.27s 
473828     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqSubEQ 
474580     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqSubEQ 
474582     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 844.6ns 
474583     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqReverseEQ.proof 
474583     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 56.4ns 
474584     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
476851     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.27s 
476851     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqReverseEQ 
477601     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqReverseEQ 
477604     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.06ms 
477605     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqDefEQ.proof 
477605     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 45.6ns 
477606     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
479868     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.26s 
479868     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqDefEQ 
480622     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqDefEQ 
480624     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 998ns 
480625     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqDefEQ.proof 
480625     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 49ns 
480626     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
482902     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.28s 
482902     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqDefEQ 
483653     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqDefEQ 
483656     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.92ms 
483657     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqConcatWithSeqEmpty1.proof 
483658     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 58.4ns 
483658     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
485931     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.27s 
485931     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqConcatWithSeqEmpty1 
486683     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqConcatWithSeqEmpty1 
486689     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 5.01ms 
486691     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqConcatWithSeqEmpty2.proof 
486691     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 62.5ns 
486691     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
488962     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.27s 
488962     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqConcatWithSeqEmpty2 
489712     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqConcatWithSeqEmpty2 
489719     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 5.35ms 
489720     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqReverseOfSeqEmpty.proof 
489721     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 53.5ns 
489721     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
491988     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.27s 
491988     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqReverseOfSeqEmpty 
492738     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqReverseOfSeqEmpty 
492743     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.77ms 
492744     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_subSeqComplete.proof 
492744     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 46.9ns 
492745     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
495042     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.3s 
495042     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: subSeqComplete 
495778     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: subSeqComplete 
495783     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.76ms 
495784     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_subSeqTailR.proof 
495784     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 58ns 
495785     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
498053     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.27s 
498054     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: subSeqTailR 
498807     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: subSeqTailR 
498816     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 7.24ms 
498817     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_subSeqTailL.proof 
498818     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 58.8ns 
498818     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
501083     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.26s 
501083     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: subSeqTailL 
501832     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: subSeqTailL 
501841     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 7.18ms 
501842     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_subSeqTailEQR.proof 
501842     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 56.8ns 
501843     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
504107     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.26s 
504108     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: subSeqTailEQR 
504861     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: subSeqTailEQR 
504869     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 6.66ms 
504870     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_subSeqTailEQL.proof 
504871     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 57.7ns 
504871     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
507146     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.28s 
507146     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: subSeqTailEQL 
507897     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: subSeqTailEQL 
507903     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.5ms 
507904     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDef_split.proof 
507904     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 55.5ns 
507905     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
510169     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.26s 
510169     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_split 
510921     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDef_split 
510938     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 14.44ms 
510940     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDef_induction_upper.proof 
510940     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 52.5ns 
510940     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
513207     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.27s 
513208     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_induction_upper 
513959     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDef_induction_upper 
513979     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 16.18ms 
513980     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDef_induction_upper_concrete.proof 
513980     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 63.9ns 
513981     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
516246     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.27s 
516246     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_induction_upper_concrete 
516998     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDef_induction_upper_concrete 
517016     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 15.09ms 
517017     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDef_induction_lower.proof 
517017     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 62.2ns 
517018     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
519286     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.27s 
519286     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_induction_lower 
520044     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDef_induction_lower 
520061     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 13.74ms 
520063     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDef_induction_lower_concrete.proof 
520063     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 61.2ns 
520063     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
522347     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.28s 
522347     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_induction_lower_concrete 
523082     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDef_induction_lower_concrete 
523100     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 14.47ms 
523101     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDef_split_in_three.proof 
523101     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 59.9ns 
523102     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
525385     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.28s 
525385     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_split_in_three 
526139     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDef_split_in_three 
526182     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 36.88ms 
526184     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDef_empty.proof 
526184     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 70.9ns 
526185     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
528455     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.27s 
528455     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_empty 
529208     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDef_empty 
529212     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.44ms 
529213     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDef_one_summand.proof 
529213     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 46.4ns 
529214     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
531485     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.27s 
531485     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_one_summand 
532235     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDef_one_summand 
532239     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.71ms 
532240     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDef_lower_equals_upper.proof 
532241     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 56.1ns 
532241     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
534508     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.27s 
534508     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_lower_equals_upper 
535259     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDef_lower_equals_upper 
535262     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.67ms 
535264     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDefOfSeq.proof 
535264     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 165.5ns 
535265     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
537529     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.26s 
537529     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDefOfSeq 
538280     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDefOfSeq 
538292     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 8.78ms 
538293     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqSelfDefinitionEQ2.proof 
538293     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 54.1ns 
538294     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
540556     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.26s 
540556     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqSelfDefinitionEQ2 
541310     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqSelfDefinitionEQ2 
541316     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.75ms 
541317     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_indexOfSeqSingleton.proof 
541317     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 53.6ns 
541318     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
543597     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.28s 
543598     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: indexOfSeqSingleton 
544351     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: indexOfSeqSingleton 
544353     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.2ms 
544355     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_indexOfSeqConcatFirst.proof 
544355     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 55.3ns 
544355     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
546622     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.27s 
546622     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: indexOfSeqConcatFirst 
547372     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: indexOfSeqConcatFirst 
547381     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 6.96ms 
547382     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_indexOfSeqConcatSecond.proof 
547382     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 46.8ns 
547383     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
549671     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.29s 
549671     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: indexOfSeqConcatSecond 
550421     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: indexOfSeqConcatSecond 
550430     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 7.3ms 
550431     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_indexOfSeqSub.proof 
550432     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 57.6ns 
550432     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
552699     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.27s 
552699     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: indexOfSeqSub 
553450     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: indexOfSeqSub 
553462     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 9.57ms 
553463     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfArray2seq.proof 
553463     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 60ns 
553464     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
555727     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.26s 
555727     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfArray2seq 
556478     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfArray2seq 
556481     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 871.9ns 
556482     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getAnyOfArray2seq.proof 
556482     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 49.8ns 
556482     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
558743     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.26s 
558743     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getAnyOfArray2seq 
559494     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getAnyOfArray2seq 
559497     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.54ms 
559498     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfArray2seq.proof 
559498     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 45.5ns 
559499     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
561783     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.28s 
561784     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfArray2seq 
562535     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfArray2seq 
562540     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.43ms 
562541     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_getAnyOfNPermInv.proof 
562541     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 55.2ns 
562542     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
564810     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.27s 
564810     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getAnyOfNPermInv 
565561     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getAnyOfNPermInv 
565566     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.51ms 
565567     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqNPermRange.proof 
565567     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 44.6ns 
565567     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
567828     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.26s 
567828     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqNPermRange 
568578     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqNPermRange 
568617     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 32.49ms 
568618     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermTrans.proof 
568618     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 60.4ns 
568619     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
570883     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.26s 
570883     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermTrans 
571635     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermTrans 
571655     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 16.69ms 
571657     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermRefl.proof 
571657     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 63.8ns 
571658     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
573952     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.29s 
573952     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermRefl 
574703     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermRefl 
574713     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 8ms 
574714     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermSplit.proof 
574714     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 61.7ns 
574715     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
576979     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.26s 
576979     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermSplit 
577730     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermSplit 
577731     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 142.8ns 
577732     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqNPermRight.proof 
577732     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 43.8ns 
577733     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
579998     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.26s 
579998     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqNPermRight 
580750     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqNPermRight 
580836     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 74.14ms 
580838     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermFromSwap.proof 
580838     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 179.6ns 
580839     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
583125     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.29s 
583125     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermFromSwap 
583876     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermFromSwap 
583907     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 26.37ms 
583908     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermTransAlt0.proof 
583908     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 50ns 
583909     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
586175     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.27s 
586175     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermTransAlt0 
586929     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermTransAlt0 
586931     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 261ns 
586933     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermTransAlt1.proof 
586933     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 56.2ns 
586933     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
589212     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.28s 
589212     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermTransAlt1 
589962     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermTransAlt1 
589964     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 192.5ns 
589965     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermTransAlt2.proof 
589965     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 57.4ns 
589966     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
592228     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.26s 
592228     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermTransAlt2 
592978     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermTransAlt2 
592979     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 189.7ns 
592980     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermTransAlt3.proof 
592980     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 43.9ns 
592981     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
595242     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.26s 
595242     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermTransAlt3 
595994     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermTransAlt3 
595996     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 401.9ns 
595997     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermForall.proof 
595997     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 56.1ns 
595997     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
598278     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.28s 
598278     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermForall 
599028     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermForall 
599109     INFO  Test worker     d.u.i.k.s.SMTFocusResults Analyzing unsat core: (L_1 L_3 L_4) 
599118     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 86.98ms 
599120     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermExists.proof 
599121     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 183.9ns 
599121     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
601403     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.28s 
601403     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermExists 
602155     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermExists 
602199     INFO  Test worker     d.u.i.k.s.SMTFocusResults Analyzing unsat core: (L_1 L_3 L_5 L_6 L_7) 
602200     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 42.79ms 
602201     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm2/Taclet_schiffl_lemma_2.proof 
602201     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 57.2ns 
602202     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
604487     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.29s 
604487     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: schiffl_lemma_2 
605238     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: schiffl_lemma_2 
605239     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.6ns 
605266     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [1] goal: 0, source line: 49, command: 'macro split-prop' 
605299     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [2] goal: 3, source line: 50, command: 'rule allRight' 
605319     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [3] goal: 4, source line: 51, command: 'rule allRight' 
605327     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [4] goal: 5, source line: 52, command: 'macro split-prop' 
605344     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [5] goal: 11, source line: 53, command: 'rule 'seqPermDefLeft'' 
605345     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [6] goal: 12, source line: 54, command: 'rule 'andLeft'' 
605348     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [7] goal: 13, source line: 55, command: 'rule 'exLeft'' 
605349     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [8] goal: 14, source line: 56, command: 'macro split-prop' 
605355     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [9] goal: 16, source line: 58, command: 'rule  seqNPermRange' 
605358     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' 
605361     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [11] goal: 18, source line: 60, command: 'rule impLeft' 
605364     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [12] goal: 19, source line: 61, command: 'tryclose branch' 
605608     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [13] goal: 20, source line: 62, command: 'rule andLeft' 
605609     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [14] goal: 97, source line: 63, command: 'rule andLeft' 
605612     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [15] goal: 98, source line: 65, command: 'instantiate var=iv with='v_y_0' occ=1' 
605613     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [16] goal: 99, source line: 66, command: 'rule impLeft' 
605614     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [17] goal: 100, source line: 67, command: 'tryclose branch' 
605749     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [18] goal: 101, source line: 68, command: 'rule andLeft' 
605750     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [19] goal: 188, source line: 69, command: 'rule andLeft' 
605753     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [20] goal: 189, source line: 71, command: 'rule seqNPermDefLeft' 
605754     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' 
605755     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [22] goal: 191, source line: 73, command: 'rule impLeft' 
605758     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [23] goal: 192, source line: 74, command: 'tryclose branch' 
605923     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [24] goal: 193, source line: 75, command: 'rule exLeft' 
605925     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [25] goal: 310, source line: 76, command: 'rule andLeft' 
605926     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [26] goal: 311, source line: 77, command: 'rule andLeft' 
605927     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [27] goal: 312, source line: 79, command: 'instantiate hide var=iv with='v_y_0' occ=2' 
605928     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [28] goal: 313, source line: 80, command: 'rule impLeft' 
605931     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [29] goal: 314, source line: 81, command: 'tryclose branch' 
606055     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [30] goal: 315, source line: 82, command: 'rule exLeft' 
606056     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [31] goal: 420, source line: 83, command: 'rule andLeft' 
606057     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [32] goal: 421, source line: 84, command: 'rule andLeft' 
606058     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [33] goal: 422, source line: 86, command: 'instantiate var=iv with='jv_0' occ=1' 
606059     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [34] goal: 423, source line: 87, command: 'rule impLeft' 
606060     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [35] goal: 424, source line: 88, command: 'tryclose branch' 
606068     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [36] goal: 425, source line: 89, command: 'rule andLeft' 
606069     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [37] goal: 434, source line: 90, command: 'rule andLeft' 
606070     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' 
606071     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [39] goal: 436, source line: 93, command: 'instantiate hide var=iv with='jv_1' occ=1' 
606072     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [40] goal: 437, source line: 94, command: 'rule impLeft' 
606073     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [41] goal: 438, source line: 95, command: 'tryclose branch' 
606080     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [42] goal: 439, source line: 96, command: 'rule andLeft' 
606081     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [43] goal: 448, source line: 97, command: 'rule andLeft' 
606085     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' 
606085     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [45] goal: 450, source line: 100, command: 'instantiate var=iv  with='v_x_0'' 
606086     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [46] goal: 451, source line: 101, command: 'rule impLeft' 
606087     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [47] goal: 452, source line: 102, command: 'tryclose branch' 
606235     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [48] goal: 453, source line: 104, command: 'instantiate var=iv  with='v_y_0'' 
606236     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [49] goal: 562, source line: 105, command: 'rule impLeft' 
606237     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [50] goal: 563, source line: 106, command: 'tryclose branch' 
606344     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [51] goal: 564, source line: 108, command: 'cut 'v_x_0 = v_y_0'' 
606344     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [52] goal: 674, source line: 110, command: 'instantiate hide var='v_r' with='seqSwap(s_0,v_x_0,jv_0)'' 
606345     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [53] goal: 676, source line: 112, command: 'rule andRight' 
606347     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [54] goal: 677, source line: 113, command: 'rule andRight' 
606348     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [55] goal: 679, source line: 114, command: 'rule andRight' 
606349     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [56] goal: 681, source line: 115, command: 'rule andRight' 
606352     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [57] goal: 683, source line: 116, command: 'rule lenOfSwap' 
606353     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [58] goal: 685, source line: 117, command: 'tryclose branch' 
606356     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [59] goal: 684, source line: 119, command: 'rule seqNPermSwapNPerm' 
606357     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' 
606358     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [61] goal: 688, source line: 121, command: 'instantiate hide var='jv' with='jv_0'' 
606359     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [62] goal: 689, source line: 122, command: 'rule impLeft' 
606360     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [63] goal: 690, source line: 123, command: 'tryclose branch' 
606452     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [64] goal: 691, source line: 124, command: 'tryclose branch' 
606455     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [65] goal: 682, source line: 126, command: 'rule allRight' 
606456     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [66] goal: 796, source line: 127, command: 'rule impRight' 
606457     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [67] goal: 797, source line: 128, command: 'rule andLeft' 
606458     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [68] goal: 798, source line: 129, command: 'instantiate var=iv with='v_iv_0'' 
606458     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [69] goal: 799, source line: 130, command: 'rule impLeft' 
606463     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [70] goal: 800, source line: 131, command: 'tryclose branch' 
606568     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [71] goal: 801, source line: 132, command: 'rule getOfSwap' 
606569     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [72] goal: 912, source line: 133, command: 'rule ifthenelse_negated' 
606570     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [73] goal: 913, source line: 134, command: 'rule ifthenelse_split occ=0' 
606571     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [74] goal: 914, source line: 135, command: 'rule andLeft' 
606574     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [75] goal: 916, source line: 136, command: 'rule andLeft' 
606574     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [76] goal: 917, source line: 137, command: 'rule andLeft' 
606575     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [77] goal: 918, source line: 138, command: 'rule ifthenelse_split occ=0' 
606576     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [78] goal: 919, source line: 139, command: 'tryclose branch' 
606665     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [79] goal: 920, source line: 140, command: 'rule ifthenelse_split occ=0' 
606667     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [80] goal: 1011, source line: 141, command: 'tryclose branch' 
606742     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [81] goal: 1012, source line: 142, command: 'tryclose branch' 
606746     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [82] goal: 915, source line: 143, command: 'tryclose branch' 
606751     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [83] goal: 680, source line: 145, command: 'rule getOfSwap' 
606752     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [84] goal: 1099, source line: 146, command: 'rule ifthenelse_negated' 
606753     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [85] goal: 1100, source line: 147, command: 'rule ifthenelse_split occ=0' 
606754     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [86] goal: 1101, source line: 148, command: 'rule andLeft' 
606755     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [87] goal: 1103, source line: 149, command: 'rule andLeft' 
606755     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [88] goal: 1104, source line: 150, command: 'rule andLeft' 
606756     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [89] goal: 1105, source line: 151, command: 'rule ifthenelse_split occ=0' 
606756     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [90] goal: 1106, source line: 152, command: 'tryclose branch' 
606764     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [91] goal: 1107, source line: 153, command: 'tryclose branch' 
606768     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [92] goal: 1102, source line: 154, command: 'tryclose branch' 
606847     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [93] goal: 678, source line: 156, command: 'rule getOfSwap' 
606848     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [94] goal: 1225, source line: 157, command: 'rule ifthenelse_negated' 
606850     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [95] goal: 1226, source line: 158, command: 'rule ifthenelse_split occ=0' 
606851     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [96] goal: 1227, source line: 159, command: 'rule andLeft' 
606853     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [97] goal: 1229, source line: 160, command: 'rule andLeft' 
606854     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [98] goal: 1230, source line: 161, command: 'rule andLeft' 
606854     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [99] goal: 1231, source line: 162, command: 'rule ifthenelse_split occ=0' 
606855     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [100] goal: 1232, source line: 163, command: 'tryclose branch' 
606898     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [101] goal: 1233, source line: 164, command: 'tryclose branch' 
606904     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [102] goal: 1228, source line: 165, command: 'tryclose branch' 
607000     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [103] goal: 675, source line: 168, command: 'cut '(int)s_0[v_x_0] = (int)s_0[v_y_0]'' 
607000     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [104] goal: 1397, source line: 169, command: 'rule seqNPermInjective' 
607002     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'' 
607003     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'' 
607004     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [107] goal: 1401, source line: 172, command: 'rule impLeft' 
607005     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [108] goal: 1402, source line: 173, command: 'tryclose branch' 
607133     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [109] goal: 1403, source line: 174, command: 'tryclose branch' 
607137     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [110] goal: 1398, source line: 176, command: 'cut '(int)s_0[v_x_0] = v_x_0'' 
607139     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [111] goal: 1534, source line: 178, command: 'instantiate hide var=v_r with='seqSwap(s_0,v_y_0,jv_1)'' 
607141     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [112] goal: 1536, source line: 180, command: 'rule andRight' 
607142     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [113] goal: 1537, source line: 181, command: 'rule andRight' 
607143     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [114] goal: 1539, source line: 182, command: 'rule andRight' 
607144     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [115] goal: 1541, source line: 183, command: 'rule andRight' 
607144     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [116] goal: 1543, source line: 184, command: 'tryclose branch' 
607153     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [117] goal: 1544, source line: 186, command: 'rule seqNPermSwapNPerm' 
607157     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'' 
607158     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [119] goal: 1559, source line: 188, command: 'instantiate hide var=jv with='jv_1'' 
607159     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [120] goal: 1560, source line: 189, command: 'tryclose branch' 
607278     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [121] goal: 1542, source line: 191, command: 'rule allRight' 
607279     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [122] goal: 1667, source line: 192, command: 'rule impRight' 
607281     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [123] goal: 1668, source line: 193, command: 'rule andLeft' 
607282     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [124] goal: 1669, source line: 194, command: 'instantiate var=iv with='v_iv_0'' 
607282     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [125] goal: 1670, source line: 195, command: 'rule impLeft' 
607283     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [126] goal: 1671, source line: 196, command: 'tryclose branch' 
607382     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [127] goal: 1672, source line: 197, command: 'rule getOfSwap' 
607383     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [128] goal: 1786, source line: 198, command: 'rule ifthenelse_negated' 
607385     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [129] goal: 1787, source line: 199, command: 'rule ifthenelse_split occ=0' 
607386     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [130] goal: 1788, source line: 200, command: 'rule andLeft' 
607386     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [131] goal: 1790, source line: 201, command: 'rule andLeft' 
607387     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [132] goal: 1791, source line: 202, command: 'rule andLeft' 
607388     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [133] goal: 1792, source line: 203, command: 'rule ifthenelse_split occ=0' 
607388     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [134] goal: 1793, source line: 204, command: 'tryclose branch' 
607463     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [135] goal: 1794, source line: 205, command: 'rule ifthenelse_split occ=0' 
607464     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [136] goal: 1885, source line: 206, command: 'tryclose branch' 
607533     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [137] goal: 1886, source line: 207, command: 'instantiate var=iv with='v_y_0'' 
607534     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [138] goal: 1968, source line: 208, command: 'rule impLeft' 
607535     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [139] goal: 1969, source line: 209, command: 'tryclose branch' 
607538     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [140] goal: 1970, source line: 210, command: 'tryclose branch' 
607542     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [141] goal: 1789, source line: 211, command: 'tryclose branch' 
607546     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [142] goal: 1540, source line: 212, command: 'tryclose branch' 
607655     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [143] goal: 1538, source line: 214, command: 'rule getOfSwap' 
607656     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [144] goal: 2097, source line: 215, command: 'rule ifthenelse_negated' 
607657     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [145] goal: 2098, source line: 216, command: 'rule ifthenelse_split occ=0' 
607658     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [146] goal: 2099, source line: 217, command: 'tryclose branch' 
607666     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [147] goal: 2100, source line: 218, command: 'tryclose branch' 
607748     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [148] goal: 1535, source line: 220, command: 'tryclose branch' 
611156     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [149] goal: 1535, source line: 223, command: 'cut  '(int)s_0[v_y_0] = v_y_0'' 
611157     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [150] goal: 4266, source line: 225, command: 'instantiate hide var=v_r with='seqSwap(s_0,v_x_0,jv_0)'' 
611161     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [151] goal: 4268, source line: 227, command: 'rule andRight' 
611164     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [152] goal: 4269, source line: 228, command: 'rule andRight' 
611165     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [153] goal: 4271, source line: 229, command: 'rule andRight' 
611166     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [154] goal: 4273, source line: 230, command: 'rule andRight' 
611167     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [155] goal: 4275, source line: 231, command: 'tryclose branch' 
611174     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [156] goal: 4276, source line: 233, command: 'rule seqNPermSwapNPerm' 
611175     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'' 
611176     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [158] goal: 4288, source line: 235, command: 'instantiate hide var=jv with='jv_0'' 
611177     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [159] goal: 4289, source line: 236, command: 'rule impLeft' 
611178     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [160] goal: 4290, source line: 237, command: 'tryclose branch' 
611266     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [161] goal: 4291, source line: 238, command: 'tryclose branch' 
611270     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [162] goal: 4274, source line: 240, command: 'rule allRight' 
611270     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [163] goal: 4400, source line: 241, command: 'rule impRight' 
611271     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [164] goal: 4401, source line: 242, command: 'rule andLeft' 
611272     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [165] goal: 4402, source line: 243, command: 'instantiate var=iv with='v_iv_0'' 
611272     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [166] goal: 4403, source line: 244, command: 'rule impLeft' 
611273     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [167] goal: 4404, source line: 245, command: 'tryclose branch' 
611364     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [168] goal: 4405, source line: 246, command: 'rule getOfSwap' 
611365     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [169] goal: 4521, source line: 247, command: 'rule ifthenelse_negated' 
611366     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [170] goal: 4522, source line: 248, command: 'rule ifthenelse_split occ=0' 
611367     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [171] goal: 4523, source line: 249, command: 'rule andLeft' 
611367     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [172] goal: 4525, source line: 250, command: 'rule andLeft' 
611368     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [173] goal: 4526, source line: 251, command: 'rule andLeft' 
611368     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [174] goal: 4527, source line: 252, command: 'rule ifthenelse_split occ=0' 
611369     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [175] goal: 4528, source line: 253, command: 'tryclose branch' 
611443     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [176] goal: 4529, source line: 254, command: 'rule ifthenelse_split occ=0' 
611444     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [177] goal: 4622, source line: 255, command: 'tryclose branch' 
611520     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [178] goal: 4623, source line: 256, command: 'tryclose branch' 
611524     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [179] goal: 4524, source line: 257, command: 'tryclose branch' 
611528     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [180] goal: 4272, source line: 259, command: 'rule getOfSwap' 
611529     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [181] goal: 4713, source line: 260, command: 'rule ifthenelse_negated' 
611530     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [182] goal: 4714, source line: 261, command: 'rule ifthenelse_split occ=0' 
611531     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [183] goal: 4715, source line: 262, command: 'tryclose branch' 
611540     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [184] goal: 4716, source line: 263, command: 'tryclose branch' 
611618     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [185] goal: 4270, source line: 265, command: 'rule getOfSwap' 
611619     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [186] goal: 4839, source line: 266, command: 'rule ifthenelse_negated' 
611620     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [187] goal: 4840, source line: 267, command: 'rule ifthenelse_split occ=0' 
611621     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [188] goal: 4841, source line: 268, command: 'tryclose branch' 
611689     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [189] goal: 4842, source line: 269, command: 'tryclose branch' 
611698     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [190] goal: 4267, source line: 272, command: 'cut '(int)s_0[v_x_0]=v_y_0'' 
611698     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [191] goal: 4948, source line: 274, command: 'instantiate hide var=v_r with='seqSwap(seqSwap(s_0,jv_0,v_x_0),jv_0,v_y_0)'' 
611699     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [192] goal: 4950, source line: 276, command: 'rule andRight' 
611701     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [193] goal: 4951, source line: 277, command: 'rule andRight' 
611701     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [194] goal: 4953, source line: 278, command: 'rule andRight' 
611702     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [195] goal: 4955, source line: 279, command: 'rule andRight' 
611702     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [196] goal: 4957, source line: 280, command: 'tryclose branch' 
611712     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [197] goal: 4958, source line: 282, command: 'rule seqNPermSwapNPerm' 
611713     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [198] goal: 4977, source line: 283, command: 'instantiate hide var=iv with='jv_0'' 
611714     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'' 
611715     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [200] goal: 4979, source line: 285, command: 'rule impLeft' 
611715     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [201] goal: 4980, source line: 286, command: 'tryclose branch' 
611798     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))'' 
611798     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [203] goal: 5093, source line: 288, command: 'instantiate hide var=iv with='jv_0'' 
611799     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'' 
611800     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [205] goal: 5095, source line: 290, command: 'rule impLeft' 
611801     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [206] goal: 5096, source line: 291, command: 'tryclose branch' 
611886     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [207] goal: 5097, source line: 292, command: 'tryclose branch' 
611890     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [208] goal: 4956, source line: 294, command: 'rule allRight' 
611891     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [209] goal: 5212, source line: 295, command: 'rule impRight' 
611895     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [210] goal: 5213, source line: 296, command: 'rule andLeft' 
611896     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [211] goal: 5214, source line: 299, command: 'instantiate var=iv with='v_iv_0'' 
611896     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [212] goal: 5215, source line: 300, command: 'rule impLeft' 
611897     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [213] goal: 5216, source line: 301, command: 'tryclose branch' 
611998     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [214] goal: 5217, source line: 303, command: 'rule getOfSwap' 
611999     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [215] goal: 5337, source line: 304, command: 'rule ifthenelse_negated' 
612000     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [216] goal: 5338, source line: 305, command: 'rule ifthenelse_split occ=0' 
612001     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [217] goal: 5339, source line: 306, command: 'rule andLeft' 
612002     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [218] goal: 5341, source line: 307, command: 'rule andLeft' 
612002     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [219] goal: 5342, source line: 308, command: 'rule andLeft' 
612003     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [220] goal: 5343, source line: 309, command: 'rule ifthenelse_split occ=0' 
612004     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [221] goal: 5344, source line: 310, command: 'rule getOfSwap' 
612004     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [222] goal: 5346, source line: 311, command: 'rule ifthenelse_negated' 
612005     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [223] goal: 5347, source line: 312, command: 'rule ifthenelse_split occ=0' 
612009     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [224] goal: 5348, source line: 313, command: 'rule andLeft' 
612009     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [225] goal: 5350, source line: 314, command: 'rule andLeft' 
612010     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [226] goal: 5351, source line: 315, command: 'rule andLeft' 
612010     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [227] goal: 5352, source line: 316, command: 'rule ifthenelse_split occ=0' 
612010     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [228] goal: 5353, source line: 317, command: 'tryclose branch' 
612092     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [229] goal: 5354, source line: 318, command: 'rule ifthenelse_split occ=0' 
612093     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [230] goal: 5463, source line: 319, command: 'tryclose branch' 
612098     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [231] goal: 5464, source line: 320, command: 'tryclose branch' 
612171     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [232] goal: 5349, source line: 321, command: 'tryclose branch' 
612246     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [233] goal: 5345, source line: 323, command: 'rule ifthenelse_split' 
612247     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [234] goal: 5660, source line: 324, command: 'rule getOfSwap' 
612247     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [235] goal: 5662, source line: 325, command: 'rule ifthenelse_negated' 
612248     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [236] goal: 5663, source line: 326, command: 'rule ifthenelse_split occ=0' 
612249     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [237] goal: 5664, source line: 327, command: 'rule andLeft' 
612249     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [238] goal: 5666, source line: 328, command: 'rule andLeft' 
612250     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [239] goal: 5667, source line: 329, command: 'rule andLeft' 
612250     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [240] goal: 5668, source line: 330, command: 'rule ifthenelse_split occ=0' 
612250     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [241] goal: 5669, source line: 331, command: 'tryclose branch' 
612331     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [242] goal: 5670, source line: 332, command: 'tryclose branch' 
612337     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [243] goal: 5665, source line: 333, command: 'tryclose branch' 
612461     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [244] goal: 5661, source line: 335, command: 'rule getOfSwap' 
612461     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [245] goal: 5887, source line: 336, command: 'rule ifthenelse_negated' 
612462     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [246] goal: 5888, source line: 337, command: 'rule ifthenelse_split occ=0' 
612464     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [247] goal: 5889, source line: 338, command: 'rule andLeft' 
612464     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [248] goal: 5891, source line: 339, command: 'rule andLeft' 
612465     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [249] goal: 5892, source line: 340, command: 'rule andLeft' 
612466     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [250] goal: 5893, source line: 341, command: 'rule ifthenelse_split occ=0' 
612466     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [251] goal: 5894, source line: 342, command: 'tryclose branch' 
612471     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [252] goal: 5895, source line: 343, command: 'rule ifthenelse_split occ=0' 
612472     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [253] goal: 5897, source line: 344, command: 'tryclose branch' 
612546     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [254] goal: 5898, source line: 345, command: 'tryclose branch' 
612551     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [255] goal: 5890, source line: 346, command: 'tryclose branch' 
612559     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [256] goal: 5340, source line: 347, command: 'tryclose branch' 
612652     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [257] goal: 4954, source line: 349, command: 'rule getOfSwap' 
612652     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [258] goal: 6115, source line: 350, command: 'rule ifthenelse_negated' 
612653     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [259] goal: 6116, source line: 351, command: 'rule ifthenelse_split occ=0' 
612654     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [260] goal: 6117, source line: 352, command: 'rule andLeft' 
612654     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [261] goal: 6119, source line: 353, command: 'rule andLeft' 
612654     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [262] goal: 6120, source line: 354, command: 'rule andLeft' 
612655     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [263] goal: 6121, source line: 355, command: 'rule ifthenelse_split occ=0' 
612655     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [264] goal: 6122, source line: 356, command: 'tryclose branch' 
612705     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [265] goal: 6123, source line: 357, command: 'rule ifthenelse_split occ=0' 
612706     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [266] goal: 6193, source line: 358, command: 'rule getOfSwap' 
612706     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [267] goal: 6195, source line: 359, command: 'rule ifthenelse_negated' 
612707     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [268] goal: 6196, source line: 360, command: 'rule ifthenelse_split occ=0' 
612707     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [269] goal: 6197, source line: 361, command: 'tryclose branch' 
612712     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [270] goal: 6198, source line: 362, command: 'tryclose branch' 
612717     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [271] goal: 6194, source line: 363, command: 'tryclose branch' 
612826     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [272] goal: 6118, source line: 364, command: 'tryclose branch' 
612907     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [273] goal: 4952, source line: 366, command: 'rule getOfSwap' 
612908     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [274] goal: 6456, source line: 367, command: 'rule ifthenelse_negated' 
612908     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [275] goal: 6457, source line: 368, command: 'rule ifthenelse_split occ=0' 
612909     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [276] goal: 6458, source line: 369, command: 'tryclose branch' 
613063     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [277] goal: 6459, source line: 370, command: 'tryclose branch' 
613145     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [278] goal: 4949, source line: 374, command: 'cut 'int::seqGet(s_0, v_y_0)=v_x_0'' 
613145     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [279] goal: 6735, source line: 377, command: 'tryclose branch' 
615932     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [280] goal: 6735, source line: 379, command: 'rule seqNPermSwapNPerm' 
615937     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [281] goal: 8783, source line: 380, command: 'instantiate hide var=iv with='jv_1'' 
615937     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'' 
615938     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [283] goal: 8785, source line: 382, command: 'rule impLeft' 
615939     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [284] goal: 8786, source line: 383, command: 'tryclose branch' 
616046     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))'' 
616047     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [286] goal: 8909, source line: 385, command: 'instantiate hide var=iv with='jv_1'' 
616048     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'' 
616048     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [288] goal: 8911, source line: 387, command: 'rule impLeft' 
616049     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [289] goal: 8912, source line: 388, command: 'tryclose branch' 
616147     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [290] goal: 8913, source line: 389, command: 'tryclose branch' 
618918     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [291] goal: 6736, source line: 396, command: 'tryclose branch' 
621874     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [292] goal: 6736, source line: 398, command: 'rule seqNPermSwapNPerm formula='seqNPerm(s_0)'' 
621878     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'' 
621879     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [294] goal: 12634, source line: 400, command: 'instantiate hide var=jv with='jv_0'' 
621879     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [295] goal: 12635, source line: 401, command: 'rule impLeft' 
621880     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [296] goal: 12636, source line: 402, command: 'tryclose branch' 
621986     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))'' 
621986     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'' 
621987     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [299] goal: 12758, source line: 405, command: 'instantiate hide var=jv with='jv_1'' 
621988     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)' ...' 
621989     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [301] goal: 12760, source line: 407, command: 'tryclose branch' 
623056     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm2/Taclet_schiffl_thm_1.proof 
623056     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 77.1ns 
623058     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
625843     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.78s 
625843     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: schiffl_thm_1 
626657     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: schiffl_thm_1 
626659     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 6.3ns 
626659     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [1] goal: 0, source line: 50, command: 'macro split-prop' 
626665     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)'' 
626674     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [3] goal: 11, source line: 52, command: 'instantiate hide var=x with='f_x'' 
626676     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [4] goal: 12, source line: 53, command: 'instantiate hide var=y with='f_y'' 
626678     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [5] goal: 13, source line: 54, command: 'rule impLeft' 
626680     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [6] goal: 14, source line: 55, command: 'tryclose branch' 
626684     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [7] goal: 15, source line: 56, command: 'rule exLeft' 
626684     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [8] goal: 23, source line: 57, command: 'macro split-prop' 
626688     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [9] goal: 27, source line: 58, command: 'rule seqPermDef occ=1' 
626688     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [10] goal: 28, source line: 59, command: 'rule andRight' 
626690     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [11] goal: 29, source line: 60, command: 'tryclose branch' 
626699     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [12] goal: 30, source line: 61, command: 'instantiate hide var=s with='r_0'' 
626699     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [13] goal: 46, source line: 62, command: 'rule andRight' 
626701     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [14] goal: 47, source line: 63, command: 'tryclose branch' 
626746     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [15] goal: 48, source line: 64, command: 'rule allRight' 
626747     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [16] goal: 119, source line: 65, command: 'rule impRight' 
626748     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [17] goal: 120, source line: 66, command: 'instantiate hide var=iv with='iv_0'' 
626748     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [18] goal: 121, source line: 67, command: 'rule impLeft' 
626749     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [19] goal: 122, source line: 68, command: 'tryclose branch' 
626809     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [20] goal: 123, source line: 69, command: 'rule andLeft' 
626809     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [21] goal: 203, source line: 70, command: 'rule seqNPermRange' 
626810     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [22] goal: 204, source line: 71, command: 'instantiate hide var=iv with='iv_0'' 
626811     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [23] goal: 205, source line: 72, command: 'rule impLeft' 
626811     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [24] goal: 206, source line: 73, command: 'tryclose branch' 
626815     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [25] goal: 207, source line: 74, command: 'rule andLeft' 
626815     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [26] goal: 215, source line: 75, command: 'rule andLeft' 
626815     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [27] goal: 216, source line: 76, command: 'rule seqNPermRange' 
626816     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [28] goal: 217, source line: 77, command: 'instantiate hide var=iv with='f_x'' 
626816     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [29] goal: 218, source line: 78, command: 'rule impLeft' 
626817     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [30] goal: 219, source line: 79, command: 'tryclose branch' 
626910     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [31] goal: 220, source line: 80, command: 'rule andLeft' 
626911     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [32] goal: 311, source line: 81, command: 'rule andLeft' 
626911     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [33] goal: 312, source line: 82, command: 'rule seqNPermRange' 
626911     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [34] goal: 313, source line: 83, command: 'instantiate hide var=iv with='f_y'' 
626912     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [35] goal: 314, source line: 84, command: 'rule impLeft' 
626913     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [36] goal: 315, source line: 85, command: 'tryclose branch' 
626991     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [37] goal: 316, source line: 86, command: 'rule andLeft' 
626991     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [38] goal: 410, source line: 87, command: 'rule andLeft' 
626992     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [39] goal: 411, source line: 88, command: 'rule getOfSeqDef occ=0' 
626992     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [40] goal: 412, source line: 89, command: 'rule getOfSeqDef' 
626992     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [41] goal: 413, source line: 90, command: 'rule ifthenelse_split occ=0' 
626993     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [42] goal: 414, source line: 91, command: 'rule andLeft occ=0' 
626993     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [43] goal: 416, source line: 92, command: 'rule sub_zero_2 occ=0' 
626994     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [44] goal: 417, source line: 93, command: 'rule ifthenelse_split occ=2' 
626994     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [45] goal: 418, source line: 94, command: 'rule andLeft' 
626994     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [46] goal: 420, source line: 95, command: 'rule sub_zero_2 occ=0' 
626995     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [47] goal: 421, source line: 96, command: 'rule add_zero_right occ=0' 
626995     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [48] goal: 422, source line: 97, command: 'rule add_zero_right occ=0' 
626995     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [49] goal: 423, source line: 98, command: 'rule add_zero_right occ=0' 
626995     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [50] goal: 424, source line: 99, command: 'rule add_zero_right occ=0' 
626996     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [51] goal: 425, source line: 100, command: 'rule add_zero_right occ=0' 
626996     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [52] goal: 426, source line: 101, command: 'rule add_zero_right occ=0' 
626996     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [53] goal: 427, source line: 102, command: 'rule ifthenelse_split occ=0' 
626997     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [54] goal: 428, source line: 103, command: 'rule ifthenelse_split occ=0' 
626997     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [55] goal: 430, source line: 104, command: 'tryclose branch' 
627000     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [56] goal: 431, source line: 105, command: 'tryclose branch' 
627035     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [57] goal: 429, source line: 106, command: 'rule ifthenelse_split occ=0' 
627035     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [58] goal: 473, source line: 107, command: 'tryclose branch' 
627090     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [59] goal: 474, source line: 108, command: 'rule ifthenelse_split occ=0' 
627091     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [60] goal: 541, source line: 109, command: 'rule seqNPermInjective' 
627091     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [61] goal: 543, source line: 110, command: 'instantiate hide var=iv with='iv_0'' 
627092     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [62] goal: 544, source line: 111, command: 'instantiate hide var=jv with='f_y'' 
627093     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [63] goal: 545, source line: 112, command: 'rule impLeft' 
627094     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [64] goal: 546, source line: 113, command: 'tryclose branch' 
627140     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [65] goal: 547, source line: 114, command: 'tryclose branch' 
627142     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [66] goal: 542, source line: 115, command: 'rule ifthenelse_split occ=0' 
627142     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [67] goal: 606, source line: 116, command: 'rule seqNPermInjective' 
627143     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [68] goal: 608, source line: 117, command: 'instantiate hide var=iv with='iv_0'' 
627144     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [69] goal: 609, source line: 118, command: 'instantiate hide var=jv with='f_x'' 
627145     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [70] goal: 610, source line: 119, command: 'rule impLeft' 
627145     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [71] goal: 611, source line: 120, command: 'tryclose branch' 
627185     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [72] goal: 612, source line: 121, command: 'tryclose branch' 
627187     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [73] goal: 607, source line: 122, command: 'tryclose branch' 
627190     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [74] goal: 419, source line: 123, command: 'tryclose branch' 
627236     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [75] goal: 415, source line: 124, command: 'tryclose branch' 
627283     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_eqSameSeq.proof 
627283     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 70.4ns 
627284     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
629524     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.24s 
629524     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: eqSameSeq 
630291     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: eqSameSeq 
630306     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 11.73ms