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

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

tests
0

failures
0

ignored
14m10.38s

duration
100%

successful

Tests

Test Method name Duration Result
powPositive data()[100] 4.079s passed
powPositiveConcrete data()[101] 4.160s passed
powGeq1Concrete data()[102] 4.116s passed
pow2InIntLower data()[103] 4.221s passed
pow2InIntUpper data()[104] 4.231s passed
logSelfConcrete data()[105] 4.233s passed
log1Concrete data()[106] 4.139s passed
logProduct data()[107] 4.066s passed
logTimesBaseConcrete data()[108] 4.057s passed
logProdIdentity data()[109] 4.293s passed
moduloByteIsInByte data()[10] 4.125s passed
logProdIdentityConcrete data()[110] 4.123s passed
logPowIdentity data()[111] 4.151s passed
logPowIdentityConcrete data()[112] 3.981s passed
logPositive data()[113] 3.990s passed
logPositiveConcrete data()[114] 4.169s passed
logMono data()[115] 4.184s passed
logMonoConcrete data()[116] 4.166s passed
powLogLess data()[117] 4.135s passed
powLogMore2 data()[118] 4.050s passed
logLessThanPow data()[119] 4.063s passed
moduloCharIsInChar data()[11] 4.149s passed
logLessThanPowConcrete data()[120] 4.071s passed
logSqueeze data()[121] 4.132s passed
ifthenelse_equals data()[122] 4.247s passed
ifthenelse_equals_1 data()[123] 4.223s passed
ifthenelse_equals_2 data()[124] 4.252s passed
disjointWithSingleton1 data()[125] 4.169s passed
disjointWithSingleton2 data()[126] 4.169s passed
disjointArrayRanges data()[127] 4.069s passed
disjointArrayRangeAllFields1 data()[128] 4.103s passed
disjointArrayRangeAllFields2 data()[129] 4.083s passed
div_unique1 data()[12] 4.089s passed
seqSelfDefinition data()[130] 4.155s passed
seqOutsideValue data()[131] 4.059s passed
castedGetAny data()[132] 4.156s passed
seqGetAlphaCast data()[133] 4.113s passed
getOfSeqSingleton data()[134] 4.174s passed
getOfSeqSingletonConcrete data()[135] 4.013s passed
getOfSeqConcat data()[136] 4.130s passed
getOfSeqSub data()[137] 4.187s passed
getOfSeqReverse data()[138] 4.025s passed
lenOfSeqEmpty data()[139] 4.075s passed
div_unique2 data()[13] 4.138s passed
lenOfSeqSingleton data()[140] 4.116s passed
lenOfSeqConcat data()[141] 4.152s passed
lenOfSeqSub data()[142] 4.109s passed
lenOfSeqReverse data()[143] 4.179s passed
equalityToSeqGetAndSeqLenLeft data()[144] 4.125s passed
equalityToSeqGetAndSeqLenRight data()[145] 4.157s passed
getOfSeqSingletonEQ data()[146] 4.130s passed
getOfSeqConcatEQ data()[147] 4.148s passed
getOfSeqSubEQ data()[148] 4.107s passed
getOfSeqReverseEQ data()[149] 3.974s passed
div_exists data()[14] 4.292s passed
lenOfSeqEmptyEQ data()[150] 4.091s passed
lenOfSeqSingletonEQ data()[151] 4.214s passed
lenOfSeqConcatEQ data()[152] 4.069s passed
lenOfSeqSubEQ data()[153] 4.099s passed
lenOfSeqReverseEQ data()[154] 4.119s passed
getOfSeqDefEQ data()[155] 4.269s passed
lenOfSeqDefEQ data()[156] 4.228s passed
seqConcatWithSeqEmpty1 data()[157] 4.158s passed
seqConcatWithSeqEmpty2 data()[158] 4.198s passed
seqReverseOfSeqEmpty data()[159] 4.211s passed
div_one data()[15] 4.068s passed
subSeqComplete data()[160] 4.324s passed
subSeqTailR data()[161] 4.133s passed
subSeqTailL data()[162] 4.200s passed
subSeqTailEQR data()[163] 4.201s passed
subSeqTailEQL data()[164] 4.195s passed
seqDef_split data()[165] 4.260s passed
seqDef_induction_upper data()[166] 4.067s passed
seqDef_induction_upper_concrete data()[167] 4.133s passed
seqDef_induction_lower data()[168] 4.221s passed
seqDef_induction_lower_concrete data()[169] 4.406s passed
jdiv_one data()[16] 3.981s passed
seqDef_split_in_three data()[170] 4.298s passed
seqDef_empty data()[171] 4.185s passed
seqDef_one_summand data()[172] 4.288s passed
seqDef_lower_equals_upper data()[173] 4.215s passed
seqDefOfSeq data()[174] 4.142s passed
seqSelfDefinitionEQ2 data()[175] 4.094s passed
indexOfSeqSingleton data()[176] 4.035s passed
indexOfSeqConcatFirst data()[177] 4.026s passed
indexOfSeqConcatSecond data()[178] 4.085s passed
indexOfSeqSub data()[179] 4.151s passed
div_zero data()[17] 4.153s passed
lenOfArray2seq data()[180] 4.201s passed
getAnyOfArray2seq data()[181] 4.186s passed
getOfArray2seq data()[182] 4.137s passed
getAnyOfNPermInv data()[183] 3.938s passed
seqNPermRange data()[184] 4.143s passed
seqPermTrans data()[185] 3.999s passed
seqPermRefl data()[186] 4.000s passed
seqPermSplit data()[187] 3.984s passed
seqNPermRight data()[188] 4.081s passed
seqPermFromSwap data()[189] 4.124s passed
divResZero1 data()[18] 4.150s passed
seqPermTransAlt0 data()[190] 4.066s passed
seqPermTransAlt1 data()[191] 4.132s passed
seqPermTransAlt2 data()[192] 4.033s passed
seqPermTransAlt3 data()[193] 4.121s passed
seqPermForall data()[194] 4.264s passed
seqPermExists data()[195] 4.256s passed
schiffl_lemma_2 data()[196] 27.764s passed
schiffl_thm_1 data()[197] 5.100s passed
eqSameSeq data()[198] 4.425s passed
divResZero2 data()[19] 4.071s passed
eqTermCut data()[1] 4.812s passed
divResOne1 data()[20] 4.106s passed
divResOne2 data()[21] 4.238s passed
div_cancel1 data()[22] 4.175s passed
div_cancel2 data()[23] 4.258s passed
divAddMultDenom data()[24] 4.829s passed
divMinus data()[25] 4.510s passed
divMinusDenom data()[26] 4.212s passed
divLeastDPos data()[27] 4.325s passed
divLeastDNeg data()[28] 4.276s passed
divGreatestDPos data()[29] 4.202s passed
equivAllRight data()[2] 4.860s passed
divGreatestDNeg data()[30] 4.207s passed
divIncreasingPos data()[31] 4.266s passed
divIncreasingNeg data()[32] 4.215s passed
jdiv_zero data()[33] 4.112s passed
jdivPulloutMinusNum data()[34] 4.027s passed
jdivPulloutMinusDenom data()[35] 4.100s passed
jdiv_uniquePosPos data()[36] 4.031s passed
jdiv_uniquePosNeg data()[37] 4.143s passed
jdiv_uniqueNegPos data()[38] 4.008s passed
jdiv_uniqueNegNeg data()[39] 4.112s passed
irrflConcrete1 data()[3] 4.695s passed
jdivMultDenom1 data()[40] 4.243s passed
jdivMultDenom2 data()[41] 4.249s passed
mod_geZero data()[42] 4.101s passed
mod_lessDenom data()[43] 4.143s passed
jmod_NumPos data()[44] 4.103s passed
jmod_NumNeg data()[45] 4.170s passed
jmod_geZero data()[46] 4.086s passed
jmodNumZero data()[47] 4.062s passed
jmod_pulloutminusNum data()[48] 4.096s passed
jmod_pulloutminusDenom data()[49] 4.101s passed
irrflConcrete2 data()[4] 4.668s passed
jmodUnique1 data()[50] 4.317s passed
jmodUnique2 data()[51] 4.219s passed
intDivRem data()[52] 4.077s passed
jmodjmod data()[53] 4.028s passed
jmodDivisible data()[54] 4.222s passed
jmodDivisibleRep data()[55] 4.043s passed
jdivAddMultDenom data()[56] 4.277s passed
jmodAltZero data()[57] 4.295s passed
jmodAddMultDenomZero data()[58] 4.158s passed
polyDiv_zero data()[59] 4.130s passed
cancel_gtPos data()[5] 4.521s passed
polyMod_ltdivDenom data()[60] 4.142s passed
bsum_empty data()[61] 4.143s passed
bsum_induction_upper data()[62] 4.033s passed
bsum_induction_lower data()[63] 4.171s passed
bsum_num_of_bounds data()[64] 4.220s passed
bsum_num_of_bounds2 data()[65] 4.082s passed
bsum_induction_upper2 data()[66] 4.051s passed
bsum_induction_upper_concrete data()[67] 4.182s passed
bsum_induction_upper_concrete_2 data()[68] 4.121s passed
bsum_induction_upper2_concrete data()[69] 4.103s passed
cancel_gtNeg data()[6] 4.356s passed
bsum_induction_lower_concrete data()[70] 4.148s passed
bsum_induction_lower2 data()[71] 4.267s passed
bsum_induction_lower2_concrete data()[72] 4.245s passed
bsum_positive data()[73] 4.263s passed
bsum_upper_bound data()[74] 4.263s passed
bsum_lower_bound data()[75] 4.219s passed
bsum_positive_lower_bound_element data()[76] 4.181s passed
bsum_sub_same_index data()[77] 4.228s passed
bsum_less_same_index data()[78] 4.225s passed
bsum_equal_except_one_index data()[79] 4.188s passed
moduloIntIsInInt data()[7] 4.423s passed
bsum_num_of_is_max data()[80] 4.092s passed
bsum_num_of_is_max2 data()[81] 4.125s passed
bsum_num_of_is_max3 data()[82] 4.301s passed
bsum_num_of_is_max4 data()[83] 4.195s passed
bsum_num_of_lt_max data()[84] 4.149s passed
bsum_num_of_lt_max2 data()[85] 4.066s passed
bsum_num_of_lt_max3 data()[86] 4.033s passed
bsum_num_of_lt_max4 data()[87] 4.115s passed
bsum_num_of_gt0 data()[88] 4.065s passed
bsum_num_of_gt0_alt data()[89] 4.072s passed
moduloLongIsInLong data()[8] 4.091s passed
bsum_add_concrete data()[90] 4.084s passed
bprod_all_positive data()[91] 4.243s passed
bprod_split data()[92] 4.156s passed
powConcrete0 data()[93] 4.171s passed
powConcrete1 data()[94] 4.171s passed
powSplitFactor data()[95] 4.227s passed
powAdd data()[96] 4.214s passed
powMono data()[97] 4.233s passed
powMonoConcrete data()[98] 4.196s passed
powMonoConcreteRight data()[99] 4.151s passed
moduloShortIsInShort data()[9] 4.057s passed

Standard output

858        INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src/test/resources/testcase/dummyTrue.key 
888        DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 10.22ms 
1135       INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
1154       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)

2329       DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for Meta 
2333       DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for Meta 
2340       DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for Meta 
2341       DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for Meta 
4214       DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for JavaBigintExpression 
11988      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 10.85s 
12074      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof dummyTrue.key 
12119      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 37ns 
12133      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/firstOrder/Taclet_eqTermCut.proof 
12133      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 173.6ns 
12138      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
15724      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.59s 
15727      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: eqTermCut 
16896      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: eqTermCut 
16935      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 26.06ms 
16949      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/firstOrder/Taclet_equivAllRight.proof 
16949      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 249.1ns 
16953      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
20545      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.59s 
20551      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: equivAllRight 
21791      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: equivAllRight 
21807      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 12.48ms 
21810      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_irrflConcrete1.proof 
21810      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 127.6ns 
21811      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
25333      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.52s 
25335      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: irrflConcrete1 
26486      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: irrflConcrete1 
26499      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 5.8ms 
26506      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_irrflConcrete2.proof 
26506      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 462.8ns 
26508      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
30001      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.49s 
30002      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: irrflConcrete2 
31158      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: irrflConcrete2 
31172      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 8.53ms 
31174      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_cancel_gtPos.proof 
31174      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 131.6ns 
31179      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
34522      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.34s 
34523      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: cancel_gtPos 
35643      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: cancel_gtPos 
35692      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 44.99ms 
35696      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_cancel_gtNeg.proof 
35697      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 587.1ns 
35699      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
38942      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.24s 
38942      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: cancel_gtNeg 
40026      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: cancel_gtNeg 
40049      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 18.56ms 
40067      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intRulesIgnoringOF/Taclet_moduloIntIsInInt.proof 
40067      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 450.5ns 
40070      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
43441      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.37s 
43442      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: moduloIntIsInInt 
44476      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: moduloIntIsInInt 
44481      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 996.4ns 
44483      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intRulesIgnoringOF/Taclet_moduloLongIsInLong.proof 
44484      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 322.5ns 
44485      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
47527      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.04s 
47530      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: moduloLongIsInLong 
48568      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: moduloLongIsInLong 
48572      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 668.7ns 
48576      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intRulesIgnoringOF/Taclet_moduloShortIsInShort.proof 
48576      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 350.4ns 
48578      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
51648      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.07s 
51649      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: moduloShortIsInShort 
52626      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: moduloShortIsInShort 
52630      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 708.6ns 
52633      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intRulesIgnoringOF/Taclet_moduloByteIsInByte.proof 
52633      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 342ns 
52634      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
55723      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.09s 
55725      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: moduloByteIsInByte 
56753      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: moduloByteIsInByte 
56756      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 653.3ns 
56760      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intRulesIgnoringOF/Taclet_moduloCharIsInChar.proof 
56760      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 365.6ns 
56761      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
59893      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.13s 
59894      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: moduloCharIsInChar 
60902      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: moduloCharIsInChar 
60906      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 855ns 
60909      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_div_unique1.proof 
60912      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 2.22ms 
60913      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
63948      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.03s 
63948      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: div_unique1 
64898      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: div_unique1 
64993      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 83.06ms 
64999      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_div_unique2.proof 
65000      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 884.2ns 
65003      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
68075      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.07s 
68076      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: div_unique2 
69063      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: div_unique2 
69132      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 64.03ms 
69137      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_div_exists.proof 
69138      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 645.8ns 
69141      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
72268      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.13s 
72268      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: div_exists 
73241      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: div_exists 
73426      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 175.47ms 
73432      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_div_one.proof 
73433      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 367.4ns 
73434      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
76485      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.05s 
76485      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: div_one 
77491      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: div_one 
77498      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.29ms 
77501      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdiv_one.proof 
77501      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 125.4ns 
77502      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
80508      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.01s 
80510      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdiv_one 
81475      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdiv_one 
81480      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.55ms 
81485      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_div_zero.proof 
81485      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 371.3ns 
81486      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
84509      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.02s 
84510      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: div_zero 
85585      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: div_zero 
85634      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 43.74ms 
85637      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divResZero1.proof 
85638      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 352.3ns 
85639      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
88817      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.18s 
88818      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divResZero1 
89766      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divResZero1 
89785      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 13.57ms 
89788      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divResZero2.proof 
89790      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 1.32ms 
89791      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
92843      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.05s 
92843      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divResZero2 
93842      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divResZero2 
93856      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 11.21ms 
93858      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divResOne1.proof 
93858      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 136.4ns 
93859      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
96901      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.04s 
96902      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divResOne1 
97939      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divResOne1 
97958      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 15.94ms 
97964      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divResOne2.proof 
97964      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 148.2ns 
97966      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
101190     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.22s 
101191     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divResOne2 
102183     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divResOne2 
102199     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 12.62ms 
102203     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_div_cancel1.proof 
102203     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 335.4ns 
102204     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
105330     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.13s 
105331     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: div_cancel1 
106352     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: div_cancel1 
106376     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 19.41ms 
106378     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_div_cancel2.proof 
106378     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 105.7ns 
106379     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
109518     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.14s 
109518     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: div_cancel2 
110630     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: div_cancel2 
110634     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.58ms 
110636     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divAddMultDenom.proof 
110637     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 256.5ns 
110638     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
114388     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.75s 
114388     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divAddMultDenom 
115415     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divAddMultDenom 
115463     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 40.85ms 
115465     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divMinus.proof 
115465     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 210.9ns 
115467     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
118781     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.31s 
118781     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divMinus 
119865     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divMinus 
119969     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 93.04ms 
119975     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divMinusDenom.proof 
119978     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 195.9ns 
119979     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
123150     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.17s 
123150     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divMinusDenom 
124144     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divMinusDenom 
124185     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 35.04ms 
124187     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divLeastDPos.proof 
124187     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 87.8ns 
124188     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
127446     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.26s 
127447     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divLeastDPos 
128497     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divLeastDPos 
128507     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 8.33ms 
128512     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divLeastDNeg.proof 
128513     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 838.1ns 
128515     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
131718     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.2s 
131718     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divLeastDNeg 
132766     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divLeastDNeg 
132785     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 15.49ms 
132791     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divGreatestDPos.proof 
132791     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 484.3ns 
132793     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
135935     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.14s 
135936     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divGreatestDPos 
136974     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divGreatestDPos 
136989     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 11.28ms 
136991     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divGreatestDNeg.proof 
136991     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 109.5ns 
136992     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
140175     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.18s 
140175     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divGreatestDNeg 
141187     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divGreatestDNeg 
141196     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 6.17ms 
141198     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divIncreasingPos.proof 
141198     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 104.2ns 
141199     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
144408     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.21s 
144408     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divIncreasingPos 
145452     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divIncreasingPos 
145462     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 6.92ms 
145465     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divIncreasingNeg.proof 
145465     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 638.3ns 
145467     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
148634     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.17s 
148635     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divIncreasingNeg 
149667     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divIncreasingNeg 
149676     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 5.8ms 
149679     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdiv_zero.proof 
149680     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 555.2ns 
149681     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
152783     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.1s 
152784     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdiv_zero 
153784     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdiv_zero 
153789     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.97ms 
153792     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdivPulloutMinusNum.proof 
153792     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 299.3ns 
153793     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
156794     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3s 
156795     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdivPulloutMinusNum 
157803     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdivPulloutMinusNum 
157816     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 9.82ms 
157819     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdivPulloutMinusDenom.proof 
157819     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 300.9ns 
157821     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
160898     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.08s 
160899     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdivPulloutMinusDenom 
161859     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdivPulloutMinusDenom 
161915     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 38.74ms 
161918     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdiv_uniquePosPos.proof 
161919     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 309.6ns 
161920     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
164952     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.03s 
164953     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdiv_uniquePosPos 
165925     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdiv_uniquePosPos 
165948     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 16.08ms 
165951     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdiv_uniquePosNeg.proof 
165951     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 425.4ns 
165952     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
169073     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.12s 
169073     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdiv_uniquePosNeg 
170068     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdiv_uniquePosNeg 
170091     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 17.38ms 
170093     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdiv_uniqueNegPos.proof 
170093     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 92.7ns 
170094     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
173104     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.01s 
173104     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdiv_uniqueNegPos 
174078     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdiv_uniqueNegPos 
174099     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 17.48ms 
174101     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdiv_uniqueNegNeg.proof 
174101     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 113.9ns 
174102     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
177202     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.1s 
177202     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdiv_uniqueNegNeg 
178192     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdiv_uniqueNegNeg 
178212     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 16.3ms 
178213     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdivMultDenom1.proof 
178213     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 86.3ns 
178214     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
181399     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.18s 
181399     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdivMultDenom1 
182408     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdivMultDenom1 
182454     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 40.2ms 
182457     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdivMultDenom2.proof 
182457     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 161.5ns 
182458     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
185613     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.16s 
185614     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdivMultDenom2 
186699     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdivMultDenom2 
186703     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.32ms 
186705     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_mod_geZero.proof 
186705     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 171.4ns 
186706     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
189777     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.07s 
189777     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: mod_geZero 
190799     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: mod_geZero 
190804     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.81ms 
190806     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_mod_lessDenom.proof 
190806     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 103.4ns 
190807     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
193963     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.16s 
193964     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: mod_lessDenom 
194937     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: mod_lessDenom 
194947     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 6.94ms 
194949     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmod_NumPos.proof 
194949     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 86.6ns 
194950     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
198054     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.1s 
198054     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmod_NumPos 
199041     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmod_NumPos 
199050     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 6.98ms 
199052     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmod_NumNeg.proof 
199052     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 68.6ns 
199053     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
202186     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.13s 
202186     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmod_NumNeg 
203195     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmod_NumNeg 
203220     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 20.89ms 
203223     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmod_geZero.proof 
203223     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 97.3ns 
203224     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
206308     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.08s 
206309     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmod_geZero 
207294     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmod_geZero 
207306     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 8.58ms 
207308     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmodNumZero.proof 
207308     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 86.4ns 
207309     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
210343     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.03s 
210344     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmodNumZero 
211364     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmodNumZero 
211369     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.34ms 
211371     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmod_pulloutminusNum.proof 
211372     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 359.4ns 
211373     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
214435     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.06s 
214436     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmod_pulloutminusNum 
215460     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmod_pulloutminusNum 
215465     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.22ms 
215466     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmod_pulloutminusDenom.proof 
215466     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 74.1ns 
215467     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
218571     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.1s 
218572     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmod_pulloutminusDenom 
219561     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmod_pulloutminusDenom 
219566     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.78ms 
219568     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmodUnique1.proof 
219568     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 83.9ns 
219569     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
222758     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.19s 
222759     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmodUnique1 
223772     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmodUnique1 
223883     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 101.07ms 
223889     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmodUnique2.proof 
223889     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 128.2ns 
223890     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
227002     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.11s 
227002     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmodUnique2 
227995     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmodUnique2 
228105     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 100.18ms 
228108     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_intDivRem.proof 
228108     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 232.7ns 
228109     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
231181     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.07s 
231181     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: intDivRem 
232178     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: intDivRem 
232183     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.07ms 
232185     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmodjmod.proof 
232186     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 285.4ns 
232188     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
235214     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.03s 
235215     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmodjmod 
236158     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmodjmod 
236210     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 38.8ms 
236213     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmodDivisible.proof 
236213     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 99.4ns 
236214     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
239367     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.15s 
239367     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmodDivisible 
240385     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmodDivisible 
240433     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 42.33ms 
240435     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmodDivisibleRep.proof 
240435     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 82ns 
240436     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
243488     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.05s 
243488     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmodDivisibleRep 
244472     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmodDivisibleRep 
244476     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.63ms 
244477     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdivAddMultDenom.proof 
244478     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 59.1ns 
244479     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
247527     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.05s 
247528     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdivAddMultDenom 
248534     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdivAddMultDenom 
248751     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 204.95ms 
248755     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmodAltZero.proof 
248756     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 410.8ns 
248757     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
252028     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.27s 
252028     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmodAltZero 
253036     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmodAltZero 
253048     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 10.18ms 
253050     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmodAddMultDenomZero.proof 
253050     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 103.5ns 
253051     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
256226     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.17s 
256226     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmodAddMultDenomZero 
257196     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmodAddMultDenomZero 
257207     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 7.43ms 
257209     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_polyDiv_zero.proof 
257209     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 88.8ns 
257210     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
260320     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.11s 
260320     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: polyDiv_zero 
261316     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: polyDiv_zero 
261336     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 17.08ms 
261338     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_polyMod_ltdivDenom.proof 
261338     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 92ns 
261339     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
264428     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.09s 
264428     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: polyMod_ltdivDenom 
265455     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: polyMod_ltdivDenom 
265477     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 9.42ms 
265481     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_empty.proof 
265482     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 318.8ns 
265483     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
268637     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.15s 
268638     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_empty 
269618     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_empty 
269623     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.18ms 
269624     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_induction_upper.proof 
269624     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 143ns 
269625     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
272690     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.06s 
272690     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_upper 
273650     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_induction_upper 
273655     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.97ms 
273657     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_induction_lower.proof 
273657     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 62.3ns 
273658     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
276767     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.11s 
276767     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_lower 
277805     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_induction_lower 
277826     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 18.39ms 
277828     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_bounds.proof 
277828     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 78.3ns 
277829     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
280990     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.16s 
280991     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_bounds 
282025     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_bounds 
282046     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 16.76ms 
282047     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_bounds2.proof 
282047     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 68.1ns 
282049     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
285121     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.07s 
285121     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_bounds2 
286110     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_bounds2 
286128     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 15.24ms 
286130     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_induction_upper2.proof 
286130     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 114.1ns 
286131     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
289150     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.02s 
289150     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_upper2 
290176     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_induction_upper2 
290180     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.38ms 
290181     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_induction_upper_concrete.proof 
290181     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 71.1ns 
290182     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
293370     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.19s 
293370     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_upper_concrete 
294357     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_induction_upper_concrete 
294362     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.59ms 
294363     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_induction_upper_concrete_2.proof 
294363     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 94.8ns 
294364     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
297498     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.13s 
297498     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_upper_concrete_2 
298476     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_induction_upper_concrete_2 
298482     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.22ms 
298484     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_induction_upper2_concrete.proof 
298484     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 74.1ns 
298485     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
301581     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.1s 
301581     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_upper2_concrete 
302581     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_induction_upper2_concrete 
302585     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.31ms 
302587     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_induction_lower_concrete.proof 
302587     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 70.8ns 
302588     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
305680     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.09s 
305681     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_lower_concrete 
306731     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_induction_lower_concrete 
306733     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 657.4ns 
306735     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_induction_lower2.proof 
306735     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 62.8ns 
306736     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
309971     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.23s 
309971     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_lower2 
310994     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_induction_lower2 
311000     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.57ms 
311002     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_induction_lower2_concrete.proof 
311002     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 83ns 
311003     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
314221     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.22s 
314221     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_lower2_concrete 
315242     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_induction_lower2_concrete 
315245     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.23ms 
315248     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_positive.proof 
315248     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 234.9ns 
315249     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
318429     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.18s 
318429     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_positive 
319435     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_positive 
319507     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 68.64ms 
319511     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_upper_bound.proof 
319511     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 261.3ns 
319512     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
322699     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.19s 
322699     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_upper_bound 
323734     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_upper_bound 
323771     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 33.14ms 
323773     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_lower_bound.proof 
323773     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 67.8ns 
323774     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
326939     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.16s 
326939     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_lower_bound 
327955     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_lower_bound 
327991     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 31.88ms 
327992     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_positive_lower_bound_element.proof 
327992     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 76.2ns 
327993     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
331120     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.13s 
331121     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_positive_lower_bound_element 
332121     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_positive_lower_bound_element 
332170     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 43.23ms 
332173     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_sub_same_index.proof 
332174     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 241.5ns 
332175     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
335338     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.16s 
335339     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_sub_same_index 
336366     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_sub_same_index 
336397     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 27.76ms 
336401     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_less_same_index.proof 
336401     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 85.2ns 
336402     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
339526     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.12s 
339526     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_less_same_index 
340569     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_less_same_index 
340624     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 49.95ms 
340625     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_equal_except_one_index.proof 
340626     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 64.4ns 
340626     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
343776     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.15s 
343777     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_equal_except_one_index 
344785     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_equal_except_one_index 
344812     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 23.88ms 
344814     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_is_max.proof 
344814     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 93.3ns 
344815     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
347893     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.08s 
347893     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_is_max 
348881     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_is_max 
348904     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 19.72ms 
348910     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_is_max2.proof 
348918     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 110ns 
348919     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
352031     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.11s 
352031     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_is_max2 
353002     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_is_max2 
353029     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 23.23ms 
353031     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_is_max3.proof 
353031     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 78.3ns 
353032     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
356215     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.18s 
356215     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_is_max3 
357293     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_is_max3 
357330     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 33.11ms 
357332     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_is_max4.proof 
357332     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 82ns 
357333     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
360494     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.16s 
360494     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_is_max4 
361495     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_is_max4 
361525     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 25.6ms 
361527     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_lt_max.proof 
361527     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 103.2ns 
361528     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
364629     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.1s 
364630     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_lt_max 
365628     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_lt_max 
365674     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 42.79ms 
365676     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_lt_max2.proof 
365676     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 102.6ns 
365677     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
368763     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.09s 
368764     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_lt_max2 
369712     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_lt_max2 
369740     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 21.29ms 
369742     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_lt_max3.proof 
369742     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 199.4ns 
369743     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
372762     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.02s 
372762     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_lt_max3 
373750     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_lt_max3 
373773     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 20.45ms 
373775     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_lt_max4.proof 
373775     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 137.7ns 
373776     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
376878     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.1s 
376878     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_lt_max4 
377867     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_lt_max4 
377888     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 18.03ms 
377890     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_gt0.proof 
377890     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 58.4ns 
377891     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
380932     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.04s 
380932     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_gt0 
381930     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_gt0 
381953     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 19.22ms 
381954     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_gt0_alt.proof 
381955     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 79.7ns 
381955     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
385026     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.07s 
385027     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_gt0_alt 
386002     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_gt0_alt 
386025     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 19.98ms 
386027     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_add_concrete.proof 
386027     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 108.8ns 
386028     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
389099     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.07s 
389099     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_add_concrete 
390100     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_add_concrete 
390109     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 6ms 
390110     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bprod/Taclet_bprod_all_positive.proof 
390110     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 85.2ns 
390111     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
393331     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.22s 
393331     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bprod_all_positive 
394337     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bprod_all_positive 
394352     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 12.62ms 
394354     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bprod/Taclet_bprod_split.proof 
394354     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 74.8ns 
394355     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
397476     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.12s 
397476     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bprod_split 
398503     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bprod_split 
398508     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.25ms 
398509     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powConcrete0.proof 
398509     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 73.7ns 
398510     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
401640     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.13s 
401640     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powConcrete0 
402675     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powConcrete0 
402678     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 931.1ns 
402681     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powConcrete1.proof 
402681     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 67.5ns 
402681     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
405856     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.17s 
405856     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powConcrete1 
406847     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powConcrete1 
406850     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.07ms 
406851     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powSplitFactor.proof 
406851     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 55.4ns 
406852     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
410027     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.17s 
410027     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powSplitFactor 
411060     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powSplitFactor 
411077     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 5.07ms 
411079     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powAdd.proof 
411079     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 88.4ns 
411080     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
414249     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.17s 
414249     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powAdd 
415282     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powAdd 
415291     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 6.81ms 
415293     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powMono.proof 
415293     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 76.5ns 
415294     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
418498     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.2s 
418498     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powMono 
419510     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powMono 
419524     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 10.87ms 
419525     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powMonoConcrete.proof 
419526     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 68.8ns 
419526     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
422682     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.16s 
422683     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powMonoConcrete 
423716     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powMonoConcrete 
423721     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.39ms 
423722     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powMonoConcreteRight.proof 
423722     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 68.8ns 
423723     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
426896     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.17s 
426896     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powMonoConcreteRight 
427869     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powMonoConcreteRight 
427872     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 860.7ns 
427873     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powPositive.proof 
427873     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 70.2ns 
427874     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
430935     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.06s 
430936     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powPositive 
431944     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powPositive 
431950     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.6ms 
431952     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powPositiveConcrete.proof 
431952     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 72.2ns 
431953     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
435073     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.12s 
435073     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powPositiveConcrete 
436107     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powPositiveConcrete 
436110     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.07ms 
436112     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powGeq1Concrete.proof 
436112     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 58.1ns 
436113     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
439191     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.08s 
439191     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powGeq1Concrete 
440224     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powGeq1Concrete 
440227     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 735.1ns 
440228     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_pow2InIntLower.proof 
440228     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 63.6ns 
440229     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
443436     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.21s 
443436     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: pow2InIntLower 
444444     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: pow2InIntLower 
444447     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 776.4ns 
444448     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_pow2InIntUpper.proof 
444448     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 71.2ns 
444449     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
447662     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.21s 
447662     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: pow2InIntUpper 
448674     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: pow2InIntUpper 
448678     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.1ms 
448680     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logSelfConcrete.proof 
448680     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 56.8ns 
448680     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
451898     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.22s 
451898     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logSelfConcrete 
452902     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logSelfConcrete 
452911     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 7.08ms 
452913     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_log1Concrete.proof 
452913     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 68.9ns 
452913     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
456052     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.14s 
456052     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: log1Concrete 
457046     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: log1Concrete 
457050     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.14ms 
457052     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logProduct.proof 
457052     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 116.1ns 
457053     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
460107     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.05s 
460107     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logProduct 
461108     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logProduct 
461116     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 6.26ms 
461118     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logTimesBaseConcrete.proof 
461118     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 74.7ns 
461119     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
464221     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.1s 
464222     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logTimesBaseConcrete 
465169     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logTimesBaseConcrete 
465174     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.78ms 
465175     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logProdIdentity.proof 
465175     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 87.2ns 
465176     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
468418     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.24s 
468418     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logProdIdentity 
469447     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logProdIdentity 
469466     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 13.68ms 
469468     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logProdIdentityConcrete.proof 
469468     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 76.3ns 
469469     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
472584     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.12s 
472584     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logProdIdentityConcrete 
473585     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logProdIdentityConcrete 
473590     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.24ms 
473591     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logPowIdentity.proof 
473591     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 91.2ns 
473592     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
476697     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.1s 
476697     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logPowIdentity 
477736     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logPowIdentity 
477740     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.66ms 
477742     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logPowIdentityConcrete.proof 
477742     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 89.8ns 
477743     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
480741     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3s 
480741     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logPowIdentityConcrete 
481717     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logPowIdentityConcrete 
481721     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.95ms 
481723     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logPositive.proof 
481723     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 73.6ns 
481724     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
484722     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3s 
484723     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logPositive 
485692     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logPositive 
485711     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 15.41ms 
485713     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logPositiveConcrete.proof 
485713     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 144.4ns 
485714     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
488846     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.13s 
488847     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logPositiveConcrete 
489874     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logPositiveConcrete 
489879     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 374.8ns 
489882     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logMono.proof 
489882     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 58.9ns 
489883     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
493020     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.14s 
493021     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logMono 
494029     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logMono 
494064     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 30.99ms 
494066     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logMonoConcrete.proof 
494066     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 65ns 
494067     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
497236     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.17s 
497237     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logMonoConcrete 
498225     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logMonoConcrete 
498230     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.58ms 
498232     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powLogLess.proof 
498233     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 66ns 
498234     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
501355     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.12s 
501356     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powLogLess 
502346     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powLogLess 
502366     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 17.22ms 
502368     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powLogMore2.proof 
502368     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 116.9ns 
502369     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
505432     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.06s 
505432     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powLogMore2 
506397     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powLogMore2 
506416     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 15.98ms 
506418     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logLessThanPow.proof 
506418     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 91.4ns 
506418     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
509491     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.07s 
509491     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logLessThanPow 
510452     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logLessThanPow 
510479     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 23.26ms 
510481     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logLessThanPowConcrete.proof 
510481     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 78.6ns 
510482     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
513561     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.08s 
513562     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logLessThanPowConcrete 
514547     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logLessThanPowConcrete 
514550     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 686.2ns 
514551     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logSqueeze.proof 
514552     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 54.3ns 
514552     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
517672     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.12s 
517672     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logSqueeze 
518676     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logSqueeze 
518682     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.27ms 
518684     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/booleanRules/Taclet_ifthenelse_equals.proof 
518684     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 57.6ns 
518685     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
521859     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.17s 
521859     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: ifthenelse_equals 
522925     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: ifthenelse_equals 
522930     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.74ms 
522932     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/booleanRules/Taclet_ifthenelse_equals_1.proof 
522932     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 199.1ns 
522934     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
526086     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.15s 
526087     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: ifthenelse_equals_1 
527149     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: ifthenelse_equals_1 
527152     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 975ns 
527154     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/booleanRules/Taclet_ifthenelse_equals_2.proof 
527154     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 56.6ns 
527155     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
530361     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.21s 
530362     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: ifthenelse_equals_2 
531401     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: ifthenelse_equals_2 
531405     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.41ms 
531409     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/locSet/Taclet_disjointWithSingleton1.proof 
531409     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 218.8ns 
531410     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
534543     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.13s 
534543     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: disjointWithSingleton1 
535572     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: disjointWithSingleton1 
535576     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.56ms 
535578     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/locSet/Taclet_disjointWithSingleton2.proof 
535578     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 172.3ns 
535579     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
538760     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.18s 
538760     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: disjointWithSingleton2 
539740     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: disjointWithSingleton2 
539744     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.53ms 
539746     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/locSet/Taclet_disjointArrayRanges.proof 
539746     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 74.8ns 
539747     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
542803     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.06s 
542803     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: disjointArrayRanges 
543804     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: disjointArrayRanges 
543814     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 6.71ms 
543815     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/locSet/Taclet_disjointArrayRangeAllFields1.proof 
543815     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 88.6ns 
543816     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
546904     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.09s 
546904     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: disjointArrayRangeAllFields1 
547908     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: disjointArrayRangeAllFields1 
547916     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 6.42ms 
547918     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/locSet/Taclet_disjointArrayRangeAllFields2.proof 
547918     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 55.4ns 
547919     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
551029     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.11s 
551029     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: disjointArrayRangeAllFields2 
551992     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: disjointArrayRangeAllFields2 
551999     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 5.62ms 
552001     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqSelfDefinition.proof 
552001     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 67.7ns 
552002     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
555113     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.11s 
555113     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqSelfDefinition 
556140     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqSelfDefinition 
556154     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 11.3ms 
556157     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqOutsideValue.proof 
556157     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 228.3ns 
556158     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
559221     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.06s 
559221     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqOutsideValue 
560209     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqOutsideValue 
560213     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.62ms 
560215     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_castedGetAny.proof 
560215     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 82.5ns 
560216     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
563354     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.14s 
563355     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: castedGetAny 
564363     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: castedGetAny 
564369     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.4ms 
564371     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqGetAlphaCast.proof 
564371     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 88.7ns 
564372     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
567450     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.08s 
567450     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqGetAlphaCast 
568480     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqGetAlphaCast 
568482     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 827.7ns 
568484     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqSingleton.proof 
568484     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 53.8ns 
568484     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
571651     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.17s 
571651     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqSingleton 
572653     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqSingleton 
572656     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.02ms 
572657     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqSingletonConcrete.proof 
572658     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 123.1ns 
572658     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
575653     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.99s 
575654     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqSingletonConcrete 
576667     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqSingletonConcrete 
576670     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 970.9ns 
576671     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqConcat.proof 
576671     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 79.1ns 
576672     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
579789     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.12s 
579789     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqConcat 
580787     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqConcat 
580799     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 9.54ms 
580801     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqSub.proof 
580801     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 92.5ns 
580801     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
583986     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.18s 
583987     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqSub 
584983     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqSub 
584986     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.45ms 
584988     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqReverse.proof 
584988     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 51.9ns 
584988     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
588042     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.05s 
588042     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqReverse 
589002     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqReverse 
589011     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 6.21ms 
589013     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqEmpty.proof 
589013     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 270.8ns 
589014     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
592100     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.09s 
592101     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqEmpty 
593084     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqEmpty 
593087     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.04ms 
593088     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqSingleton.proof 
593088     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 76.2ns 
593089     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
596223     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.13s 
596223     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqSingleton 
597200     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqSingleton 
597202     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 752.6ns 
597203     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqConcat.proof 
597204     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 71.6ns 
597205     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
600344     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.14s 
600344     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqConcat 
601350     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqConcat 
601354     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.74ms 
601356     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqSub.proof 
601356     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 167ns 
601357     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
604426     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.07s 
604426     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqSub 
605459     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqSub 
605464     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.21ms 
605465     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqReverse.proof 
605465     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 56.4ns 
605466     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
608622     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.16s 
608622     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqReverse 
609638     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqReverse 
609642     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.52ms 
609643     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_equalityToSeqGetAndSeqLenLeft.proof 
609643     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 79.1ns 
609644     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
612757     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.11s 
612757     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: equalityToSeqGetAndSeqLenLeft 
613764     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: equalityToSeqGetAndSeqLenLeft 
613767     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.44ms 
613769     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_equalityToSeqGetAndSeqLenRight.proof 
613769     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 50ns 
613769     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
616878     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.11s 
616878     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: equalityToSeqGetAndSeqLenRight 
617919     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: equalityToSeqGetAndSeqLenRight 
617924     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.8ms 
617926     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqSingletonEQ.proof 
617926     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 96.6ns 
617926     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
620992     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.07s 
620992     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqSingletonEQ 
622050     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqSingletonEQ 
622054     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.19ms 
622056     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqConcatEQ.proof 
622056     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 55.5ns 
622056     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
625155     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.1s 
625155     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqConcatEQ 
626186     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqConcatEQ 
626202     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 12.16ms 
626204     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqSubEQ.proof 
626205     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 228.4ns 
626206     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
629315     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.11s 
629315     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqSubEQ 
630307     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqSubEQ 
630310     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 662.4ns 
630311     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqReverseEQ.proof 
630311     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 63.1ns 
630312     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
633347     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.04s 
633347     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqReverseEQ 
634276     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqReverseEQ 
634283     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.53ms 
634284     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqEmptyEQ.proof 
634284     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 64.7ns 
634285     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
637350     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.06s 
637350     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqEmptyEQ 
638368     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqEmptyEQ 
638373     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.97ms 
638376     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqSingletonEQ.proof 
638376     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 72.8ns 
638377     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
641519     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.14s 
641519     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqSingletonEQ 
642585     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqSingletonEQ 
642588     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.38ms 
642590     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqConcatEQ.proof 
642590     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 70.1ns 
642590     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
645640     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.05s 
645640     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqConcatEQ 
646653     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqConcatEQ 
646657     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.36ms 
646659     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqSubEQ.proof 
646659     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 53.5ns 
646659     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
649744     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.08s 
649744     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqSubEQ 
650754     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqSubEQ 
650757     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 999.2ns 
650759     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqReverseEQ.proof 
650759     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 66ns 
650760     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
653873     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.11s 
653873     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqReverseEQ 
654871     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqReverseEQ 
654875     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.04ms 
654876     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqDefEQ.proof 
654876     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 214ns 
654877     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
658076     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.2s 
658076     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqDefEQ 
659140     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqDefEQ 
659144     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.52ms 
659146     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqDefEQ.proof 
659146     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 52ns 
659147     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
662320     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.17s 
662320     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqDefEQ 
663367     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqDefEQ 
663372     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.08ms 
663374     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqConcatWithSeqEmpty1.proof 
663374     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 95.8ns 
663376     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
666484     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.11s 
666484     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqConcatWithSeqEmpty1 
667520     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqConcatWithSeqEmpty1 
667530     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 7.29ms 
667531     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqConcatWithSeqEmpty2.proof 
667531     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 81.8ns 
667532     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
670679     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.15s 
670679     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqConcatWithSeqEmpty2 
671718     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqConcatWithSeqEmpty2 
671728     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 7.65ms 
671730     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqReverseOfSeqEmpty.proof 
671730     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 67.9ns 
671731     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
674889     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.16s 
674890     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqReverseOfSeqEmpty 
675931     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqReverseOfSeqEmpty 
675939     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 5.93ms 
675941     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_subSeqComplete.proof 
675941     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 57.5ns 
675942     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
679221     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.28s 
679222     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: subSeqComplete 
680255     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: subSeqComplete 
680264     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 5.48ms 
680265     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_subSeqTailR.proof 
680265     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 67.1ns 
680266     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
683340     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.07s 
683340     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: subSeqTailR 
684372     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: subSeqTailR 
684396     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 20.32ms 
684397     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_subSeqTailL.proof 
684397     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 70.3ns 
684398     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
687548     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.15s 
687548     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: subSeqTailL 
688583     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: subSeqTailL 
688596     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 10.55ms 
688598     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_subSeqTailEQR.proof 
688598     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 84.6ns 
688599     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
691729     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.13s 
691729     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: subSeqTailEQR 
692785     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: subSeqTailEQR 
692797     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 10.16ms 
692799     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_subSeqTailEQL.proof 
692799     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 84.6ns 
692800     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
695924     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.12s 
695925     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: subSeqTailEQL 
696982     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: subSeqTailEQL 
696992     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 7.34ms 
696994     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDef_split.proof 
696994     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 114.1ns 
696995     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
700198     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.2s 
700198     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_split 
701225     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDef_split 
701252     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 23.99ms 
701254     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDef_induction_upper.proof 
701254     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 67.3ns 
701255     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
704330     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.07s 
704330     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_induction_upper 
705288     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDef_induction_upper 
705319     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 26.75ms 
705321     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDef_induction_upper_concrete.proof 
705321     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 73ns 
705322     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
708385     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.06s 
708385     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_induction_upper_concrete 
709426     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDef_induction_upper_concrete 
709453     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 22.55ms 
709454     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDef_induction_lower.proof 
709454     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 74.4ns 
709455     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
712623     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.17s 
712623     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_induction_lower 
713649     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDef_induction_lower 
713673     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 20.45ms 
713675     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDef_induction_lower_concrete.proof 
713675     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 53.3ns 
713676     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
716971     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.3s 
716972     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_induction_lower_concrete 
718055     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDef_induction_lower_concrete 
718079     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 20.56ms 
718081     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDef_split_in_three.proof 
718081     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 63.3ns 
718082     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
721259     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.18s 
721259     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_split_in_three 
722308     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDef_split_in_three 
722377     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 59.87ms 
722379     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDef_empty.proof 
722379     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 78.7ns 
722379     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
725536     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.16s 
725536     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_empty 
726556     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDef_empty 
726562     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.92ms 
726564     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDef_one_summand.proof 
726564     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 52.6ns 
726565     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
729799     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.23s 
729799     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_one_summand 
730844     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDef_one_summand 
730850     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.2ms 
730852     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDef_lower_equals_upper.proof 
730852     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 72.4ns 
730853     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
734060     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.21s 
734060     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_lower_equals_upper 
735061     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDef_lower_equals_upper 
735065     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.21ms 
735066     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDefOfSeq.proof 
735066     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 67.7ns 
735067     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
738158     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.09s 
738158     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDefOfSeq 
739188     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDefOfSeq 
739207     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 15.13ms 
739209     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqSelfDefinitionEQ2.proof 
739209     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 65.5ns 
739209     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
742280     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.07s 
742280     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqSelfDefinitionEQ2 
743291     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqSelfDefinitionEQ2 
743301     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 6.39ms 
743302     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_indexOfSeqSingleton.proof 
743302     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 72.3ns 
743303     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
746344     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.04s 
746344     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: indexOfSeqSingleton 
747332     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: indexOfSeqSingleton 
747336     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.79ms 
747337     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_indexOfSeqConcatFirst.proof 
747337     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 63.3ns 
747338     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
750344     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.01s 
750344     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: indexOfSeqConcatFirst 
751349     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: indexOfSeqConcatFirst 
751362     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 10.43ms 
751364     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_indexOfSeqConcatSecond.proof 
751364     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 98.2ns 
751365     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
754440     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.08s 
754441     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: indexOfSeqConcatSecond 
755434     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: indexOfSeqConcatSecond 
755448     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 11.32ms 
755449     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_indexOfSeqSub.proof 
755449     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 71ns 
755450     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
758512     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.06s 
758513     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: indexOfSeqSub 
759578     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: indexOfSeqSub 
759598     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 15.62ms 
759599     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfArray2seq.proof 
759599     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 75.2ns 
759600     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
762781     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.18s 
762782     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfArray2seq 
763795     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfArray2seq 
763799     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.65ms 
763801     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getAnyOfArray2seq.proof 
763801     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 52.5ns 
763802     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
766916     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.11s 
766916     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getAnyOfArray2seq 
767980     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getAnyOfArray2seq 
767985     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.33ms 
767987     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfArray2seq.proof 
767987     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 77ns 
767988     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
771153     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.17s 
771153     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfArray2seq 
772116     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfArray2seq 
772123     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 5.2ms 
772124     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_getAnyOfNPermInv.proof 
772124     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 98ns 
772125     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
775077     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.95s 
775077     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getAnyOfNPermInv 
776053     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getAnyOfNPermInv 
776060     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.42ms 
776062     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqNPermRange.proof 
776062     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 78.8ns 
776063     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
779137     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.07s 
779137     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqNPermRange 
780146     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqNPermRange 
780203     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 50.41ms 
780205     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermTrans.proof 
780205     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 72.9ns 
780205     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
783217     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.01s 
783217     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermTrans 
784177     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermTrans 
784202     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 21.68ms 
784204     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermRefl.proof 
784204     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 64.3ns 
784205     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
787221     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.02s 
787221     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermRefl 
788187     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermRefl 
788202     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 13.08ms 
788204     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermSplit.proof 
788204     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 131.5ns 
788205     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
791161     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.96s 
791161     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermSplit 
792184     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermSplit 
792186     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 238.9ns 
792190     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqNPermRight.proof 
792190     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 62.9ns 
792191     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
795166     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.97s 
795166     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqNPermRight 
796156     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqNPermRight 
796268     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 101.92ms 
796270     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermFromSwap.proof 
796271     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 189ns 
796272     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
799308     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.04s 
799308     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermFromSwap 
800341     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermFromSwap 
800392     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 44.6ms 
800396     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermTransAlt0.proof 
800396     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 74.2ns 
800397     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
803465     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.07s 
803465     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermTransAlt0 
804458     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermTransAlt0 
804460     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 223.3ns 
804462     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermTransAlt1.proof 
804462     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 56.6ns 
804463     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
807561     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.1s 
807561     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermTransAlt1 
808590     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermTransAlt1 
808593     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 288.4ns 
808594     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermTransAlt2.proof 
808594     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 63.8ns 
808595     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
811626     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.03s 
811626     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermTransAlt2 
812623     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermTransAlt2 
812625     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 278.9ns 
812627     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermTransAlt3.proof 
812627     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 80.8ns 
812628     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
815765     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.14s 
815765     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermTransAlt3 
816744     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermTransAlt3 
816746     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 369.2ns 
816747     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermForall.proof 
816748     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 69.2ns 
816748     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
819872     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.12s 
819872     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermForall 
820873     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermForall 
820998     INFO  Test worker     d.u.i.k.s.SMTFocusResults Analyzing unsat core: (L_1 L_3 L_4) 
821009     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 133.18ms 
821013     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermExists.proof 
821013     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 286.8ns 
821014     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
824212     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.2s 
824212     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermExists 
825218     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermExists 
825266     INFO  Test worker     d.u.i.k.s.SMTFocusResults Analyzing unsat core: (L_1 L_3 L_5 L_6 L_7) 
825267     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 47.47ms 
825269     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm2/Taclet_schiffl_lemma_2.proof 
825269     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 76.5ns 
825270     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
828370     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.1s 
828370     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: schiffl_lemma_2 
829410     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: schiffl_lemma_2 
829412     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.8ns 
829460     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [1] goal: 0, source line: 49, command: 'macro split-prop' 
829528     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [2] goal: 3, source line: 50, command: 'rule allRight' 
829545     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [3] goal: 4, source line: 51, command: 'rule allRight' 
829553     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [4] goal: 5, source line: 52, command: 'macro split-prop' 
829570     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [5] goal: 11, source line: 53, command: 'rule 'seqPermDefLeft'' 
829572     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [6] goal: 12, source line: 54, command: 'rule 'andLeft'' 
829574     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [7] goal: 13, source line: 55, command: 'rule 'exLeft'' 
829575     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [8] goal: 14, source line: 56, command: 'macro split-prop' 
829584     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [9] goal: 16, source line: 57, command: 'rule  seqNPermRange' 
829589     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' 
829594     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [11] goal: 18, source line: 60, command: 'rule impLeft' 
829598     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [12] goal: 19, source line: 61, command: 'tryclose branch' 
829909     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [13] goal: 20, source line: 62, command: 'rule andLeft' 
829910     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [14] goal: 97, source line: 63, command: 'rule andLeft' 
829913     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [15] goal: 98, source line: 64, command: 'instantiate var=iv with='v_y_0' occ=1' 
829914     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [16] goal: 99, source line: 66, command: 'rule impLeft' 
829916     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [17] goal: 100, source line: 67, command: 'tryclose branch' 
830103     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [18] goal: 101, source line: 68, command: 'rule andLeft' 
830104     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [19] goal: 188, source line: 69, command: 'rule andLeft' 
830109     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [20] goal: 189, source line: 70, command: 'rule seqNPermDefLeft' 
830110     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' 
830112     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [22] goal: 191, source line: 73, command: 'rule impLeft' 
830115     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [23] goal: 192, source line: 74, command: 'tryclose branch' 
830352     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [24] goal: 193, source line: 75, command: 'rule exLeft' 
830355     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [25] goal: 310, source line: 76, command: 'rule andLeft' 
830356     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [26] goal: 311, source line: 77, command: 'rule andLeft' 
830357     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [27] goal: 312, source line: 78, command: 'instantiate hide var=iv with='v_y_0' occ=2' 
830357     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [28] goal: 313, source line: 80, command: 'rule impLeft' 
830360     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [29] goal: 314, source line: 81, command: 'tryclose branch' 
830517     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [30] goal: 315, source line: 82, command: 'rule exLeft' 
830520     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [31] goal: 420, source line: 83, command: 'rule andLeft' 
830521     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [32] goal: 421, source line: 84, command: 'rule andLeft' 
830522     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [33] goal: 422, source line: 85, command: 'instantiate var=iv with='jv_0' occ=1' 
830522     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [34] goal: 423, source line: 87, command: 'rule impLeft' 
830524     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [35] goal: 424, source line: 88, command: 'tryclose branch' 
830542     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [36] goal: 425, source line: 89, command: 'rule andLeft' 
830543     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [37] goal: 434, source line: 90, command: 'rule andLeft' 
830545     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' 
830546     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [39] goal: 436, source line: 92, command: 'instantiate hide var=iv with='jv_1' occ=1' 
830547     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [40] goal: 437, source line: 94, command: 'rule impLeft' 
830548     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [41] goal: 438, source line: 95, command: 'tryclose branch' 
830560     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [42] goal: 439, source line: 96, command: 'rule andLeft' 
830561     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [43] goal: 448, source line: 97, command: 'rule andLeft' 
830563     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' 
830563     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [45] goal: 450, source line: 99, command: 'instantiate var=iv  with='v_x_0'' 
830565     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [46] goal: 451, source line: 101, command: 'rule impLeft' 
830566     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [47] goal: 452, source line: 102, command: 'tryclose branch' 
830721     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [48] goal: 453, source line: 103, command: 'instantiate var=iv  with='v_y_0'' 
830723     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [49] goal: 562, source line: 105, command: 'rule impLeft' 
830724     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [50] goal: 563, source line: 106, command: 'tryclose branch' 
830872     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [51] goal: 564, source line: 107, command: 'cut 'v_x_0 = v_y_0'' 
830873     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [52] goal: 674, source line: 109, command: 'instantiate hide var='v_r' with='seqSwap(s_0,v_x_0,jv_0)'' 
830874     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [53] goal: 676, source line: 111, command: 'rule andRight' 
830878     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [54] goal: 677, source line: 113, command: 'rule andRight' 
830879     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [55] goal: 679, source line: 114, command: 'rule andRight' 
830880     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [56] goal: 681, source line: 115, command: 'rule andRight' 
830882     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [57] goal: 683, source line: 116, command: 'rule lenOfSwap' 
830883     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [58] goal: 685, source line: 117, command: 'tryclose branch' 
830887     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [59] goal: 684, source line: 118, command: 'rule seqNPermSwapNPerm' 
830888     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' 
830890     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [61] goal: 688, source line: 121, command: 'instantiate hide var='jv' with='jv_0'' 
830891     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [62] goal: 689, source line: 122, command: 'rule impLeft' 
830892     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [63] goal: 690, source line: 123, command: 'tryclose branch' 
831019     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [64] goal: 691, source line: 124, command: 'tryclose branch' 
831023     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [65] goal: 682, source line: 125, command: 'rule allRight' 
831025     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [66] goal: 796, source line: 127, command: 'rule impRight' 
831026     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [67] goal: 797, source line: 128, command: 'rule andLeft' 
831027     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [68] goal: 798, source line: 129, command: 'instantiate var=iv with='v_iv_0'' 
831028     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [69] goal: 799, source line: 130, command: 'rule impLeft' 
831033     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [70] goal: 800, source line: 131, command: 'tryclose branch' 
831188     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [71] goal: 801, source line: 132, command: 'rule getOfSwap' 
831189     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [72] goal: 912, source line: 133, command: 'rule ifthenelse_negated' 
831191     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [73] goal: 913, source line: 134, command: 'rule ifthenelse_split occ=0' 
831192     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [74] goal: 914, source line: 135, command: 'rule andLeft' 
831193     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [75] goal: 916, source line: 136, command: 'rule andLeft' 
831194     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [76] goal: 917, source line: 137, command: 'rule andLeft' 
831196     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [77] goal: 918, source line: 138, command: 'rule ifthenelse_split occ=0' 
831197     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [78] goal: 919, source line: 139, command: 'tryclose branch' 
831367     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [79] goal: 920, source line: 140, command: 'rule ifthenelse_split occ=0' 
831369     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [80] goal: 1011, source line: 141, command: 'tryclose branch' 
831465     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [81] goal: 1012, source line: 142, command: 'tryclose branch' 
831469     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [82] goal: 915, source line: 143, command: 'tryclose branch' 
831474     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [83] goal: 680, source line: 144, command: 'rule getOfSwap' 
831475     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [84] goal: 1099, source line: 146, command: 'rule ifthenelse_negated' 
831478     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [85] goal: 1100, source line: 147, command: 'rule ifthenelse_split occ=0' 
831479     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [86] goal: 1101, source line: 148, command: 'rule andLeft' 
831480     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [87] goal: 1103, source line: 149, command: 'rule andLeft' 
831480     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [88] goal: 1104, source line: 150, command: 'rule andLeft' 
831481     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [89] goal: 1105, source line: 151, command: 'rule ifthenelse_split occ=0' 
831481     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [90] goal: 1106, source line: 152, command: 'tryclose branch' 
831490     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [91] goal: 1107, source line: 153, command: 'tryclose branch' 
831495     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [92] goal: 1102, source line: 154, command: 'tryclose branch' 
831600     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [93] goal: 678, source line: 155, command: 'rule getOfSwap' 
831601     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [94] goal: 1225, source line: 157, command: 'rule ifthenelse_negated' 
831603     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [95] goal: 1226, source line: 158, command: 'rule ifthenelse_split occ=0' 
831605     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [96] goal: 1227, source line: 159, command: 'rule andLeft' 
831606     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [97] goal: 1229, source line: 160, command: 'rule andLeft' 
831606     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [98] goal: 1230, source line: 161, command: 'rule andLeft' 
831607     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [99] goal: 1231, source line: 162, command: 'rule ifthenelse_split occ=0' 
831607     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [100] goal: 1232, source line: 163, command: 'tryclose branch' 
831669     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [101] goal: 1233, source line: 164, command: 'tryclose branch' 
831675     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [102] goal: 1228, source line: 165, command: 'tryclose branch' 
831777     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [103] goal: 675, source line: 166, command: 'cut '(int)s_0[v_x_0] = (int)s_0[v_y_0]'' 
831778     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [104] goal: 1397, source line: 169, command: 'rule seqNPermInjective' 
831780     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'' 
831781     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'' 
831783     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [107] goal: 1401, source line: 172, command: 'rule impLeft' 
831786     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [108] goal: 1402, source line: 173, command: 'tryclose branch' 
831957     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [109] goal: 1403, source line: 174, command: 'tryclose branch' 
831962     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [110] goal: 1398, source line: 175, command: 'cut '(int)s_0[v_x_0] = v_x_0'' 
831964     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [111] goal: 1534, source line: 177, command: 'instantiate hide var=v_r with='seqSwap(s_0,v_y_0,jv_1)'' 
831969     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [112] goal: 1536, source line: 179, command: 'rule andRight' 
831970     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [113] goal: 1537, source line: 181, command: 'rule andRight' 
831971     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [114] goal: 1539, source line: 182, command: 'rule andRight' 
831972     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [115] goal: 1541, source line: 183, command: 'rule andRight' 
831973     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [116] goal: 1543, source line: 184, command: 'tryclose branch' 
831983     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [117] goal: 1544, source line: 185, command: 'rule seqNPermSwapNPerm' 
831990     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'' 
831991     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [119] goal: 1559, source line: 188, command: 'instantiate hide var=jv with='jv_1'' 
831992     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [120] goal: 1560, source line: 189, command: 'tryclose branch' 
832101     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [121] goal: 1542, source line: 190, command: 'rule allRight' 
832102     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [122] goal: 1667, source line: 192, command: 'rule impRight' 
832103     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [123] goal: 1668, source line: 193, command: 'rule andLeft' 
832104     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [124] goal: 1669, source line: 194, command: 'instantiate var=iv with='v_iv_0'' 
832105     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [125] goal: 1670, source line: 195, command: 'rule impLeft' 
832106     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [126] goal: 1671, source line: 196, command: 'tryclose branch' 
832235     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [127] goal: 1672, source line: 197, command: 'rule getOfSwap' 
832236     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [128] goal: 1786, source line: 198, command: 'rule ifthenelse_negated' 
832237     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [129] goal: 1787, source line: 199, command: 'rule ifthenelse_split occ=0' 
832239     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [130] goal: 1788, source line: 200, command: 'rule andLeft' 
832239     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [131] goal: 1790, source line: 201, command: 'rule andLeft' 
832240     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [132] goal: 1791, source line: 202, command: 'rule andLeft' 
832241     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [133] goal: 1792, source line: 203, command: 'rule ifthenelse_split occ=0' 
832242     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [134] goal: 1793, source line: 204, command: 'tryclose branch' 
832346     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [135] goal: 1794, source line: 205, command: 'rule ifthenelse_split occ=0' 
832347     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [136] goal: 1885, source line: 206, command: 'tryclose branch' 
832443     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [137] goal: 1886, source line: 207, command: 'instantiate var=iv with='v_y_0'' 
832444     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [138] goal: 1968, source line: 208, command: 'rule impLeft' 
832444     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [139] goal: 1969, source line: 209, command: 'tryclose branch' 
832450     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [140] goal: 1970, source line: 210, command: 'tryclose branch' 
832454     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [141] goal: 1789, source line: 211, command: 'tryclose branch' 
832460     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [142] goal: 1540, source line: 212, command: 'tryclose branch' 
832635     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [143] goal: 1538, source line: 213, command: 'rule getOfSwap' 
832636     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [144] goal: 2097, source line: 215, command: 'rule ifthenelse_negated' 
832637     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [145] goal: 2098, source line: 216, command: 'rule ifthenelse_split occ=0' 
832639     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [146] goal: 2099, source line: 217, command: 'tryclose branch' 
832658     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [147] goal: 2100, source line: 218, command: 'tryclose branch' 
832774     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [148] goal: 1535, source line: 219, command: 'tryclose branch' 
837071     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [149] goal: 1535, source line: 221, command: 'cut  '(int)s_0[v_y_0] = v_y_0'' 
837072     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [150] goal: 4266, source line: 224, command: 'instantiate hide var=v_r with='seqSwap(s_0,v_x_0,jv_0)'' 
837082     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [151] goal: 4268, source line: 226, command: 'rule andRight' 
837085     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [152] goal: 4269, source line: 228, command: 'rule andRight' 
837085     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [153] goal: 4271, source line: 229, command: 'rule andRight' 
837087     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [154] goal: 4273, source line: 230, command: 'rule andRight' 
837088     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [155] goal: 4275, source line: 231, command: 'tryclose branch' 
837100     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [156] goal: 4276, source line: 232, command: 'rule seqNPermSwapNPerm' 
837101     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'' 
837102     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [158] goal: 4288, source line: 235, command: 'instantiate hide var=jv with='jv_0'' 
837102     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [159] goal: 4289, source line: 236, command: 'rule impLeft' 
837103     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [160] goal: 4290, source line: 237, command: 'tryclose branch' 
837228     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [161] goal: 4291, source line: 238, command: 'tryclose branch' 
837232     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [162] goal: 4274, source line: 239, command: 'rule allRight' 
837233     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [163] goal: 4400, source line: 241, command: 'rule impRight' 
837233     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [164] goal: 4401, source line: 242, command: 'rule andLeft' 
837235     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [165] goal: 4402, source line: 243, command: 'instantiate var=iv with='v_iv_0'' 
837235     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [166] goal: 4403, source line: 244, command: 'rule impLeft' 
837237     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [167] goal: 4404, source line: 245, command: 'tryclose branch' 
837398     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [168] goal: 4405, source line: 246, command: 'rule getOfSwap' 
837399     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [169] goal: 4521, source line: 247, command: 'rule ifthenelse_negated' 
837400     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [170] goal: 4522, source line: 248, command: 'rule ifthenelse_split occ=0' 
837403     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [171] goal: 4523, source line: 249, command: 'rule andLeft' 
837404     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [172] goal: 4525, source line: 250, command: 'rule andLeft' 
837404     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [173] goal: 4526, source line: 251, command: 'rule andLeft' 
837405     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [174] goal: 4527, source line: 252, command: 'rule ifthenelse_split occ=0' 
837406     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [175] goal: 4528, source line: 253, command: 'tryclose branch' 
837506     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [176] goal: 4529, source line: 254, command: 'rule ifthenelse_split occ=0' 
837507     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [177] goal: 4622, source line: 255, command: 'tryclose branch' 
837600     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [178] goal: 4623, source line: 256, command: 'tryclose branch' 
837609     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [179] goal: 4524, source line: 257, command: 'tryclose branch' 
837615     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [180] goal: 4272, source line: 258, command: 'rule getOfSwap' 
837615     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [181] goal: 4713, source line: 260, command: 'rule ifthenelse_negated' 
837617     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [182] goal: 4714, source line: 261, command: 'rule ifthenelse_split occ=0' 
837618     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [183] goal: 4715, source line: 262, command: 'tryclose branch' 
837632     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [184] goal: 4716, source line: 263, command: 'tryclose branch' 
837730     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [185] goal: 4270, source line: 264, command: 'rule getOfSwap' 
837731     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [186] goal: 4839, source line: 266, command: 'rule ifthenelse_negated' 
837732     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [187] goal: 4840, source line: 267, command: 'rule ifthenelse_split occ=0' 
837733     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [188] goal: 4841, source line: 268, command: 'tryclose branch' 
837829     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [189] goal: 4842, source line: 269, command: 'tryclose branch' 
837841     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [190] goal: 4267, source line: 270, command: 'cut '(int)s_0[v_x_0]=v_y_0'' 
837842     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [191] goal: 4948, source line: 273, command: 'instantiate hide var=v_r with='seqSwap(seqSwap(s_0,jv_0,v_x_0),jv_0,v_y_0)'' 
837843     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [192] goal: 4950, source line: 275, command: 'rule andRight' 
837844     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [193] goal: 4951, source line: 277, command: 'rule andRight' 
837844     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [194] goal: 4953, source line: 278, command: 'rule andRight' 
837845     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [195] goal: 4955, source line: 279, command: 'rule andRight' 
837845     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [196] goal: 4957, source line: 280, command: 'tryclose branch' 
837858     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [197] goal: 4958, source line: 281, command: 'rule seqNPermSwapNPerm' 
837859     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [198] goal: 4977, source line: 283, command: 'instantiate hide var=iv with='jv_0'' 
837860     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'' 
837861     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [200] goal: 4979, source line: 285, command: 'rule impLeft' 
837861     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [201] goal: 4980, source line: 286, command: 'tryclose branch' 
837970     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))'' 
837970     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [203] goal: 5093, source line: 288, command: 'instantiate hide var=iv with='jv_0'' 
837972     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'' 
837975     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [205] goal: 5095, source line: 290, command: 'rule impLeft' 
837979     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [206] goal: 5096, source line: 291, command: 'tryclose branch' 
838096     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [207] goal: 5097, source line: 292, command: 'tryclose branch' 
838102     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [208] goal: 4956, source line: 293, command: 'rule allRight' 
838103     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [209] goal: 5212, source line: 295, command: 'rule impRight' 
838106     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [210] goal: 5213, source line: 296, command: 'rule andLeft' 
838107     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [211] goal: 5214, source line: 297, command: 'instantiate var=iv with='v_iv_0'' 
838107     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [212] goal: 5215, source line: 300, command: 'rule impLeft' 
838108     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [213] goal: 5216, source line: 301, command: 'tryclose branch' 
838237     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [214] goal: 5217, source line: 302, command: 'rule getOfSwap' 
838238     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [215] goal: 5337, source line: 304, command: 'rule ifthenelse_negated' 
838239     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [216] goal: 5338, source line: 305, command: 'rule ifthenelse_split occ=0' 
838240     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [217] goal: 5339, source line: 306, command: 'rule andLeft' 
838241     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [218] goal: 5341, source line: 307, command: 'rule andLeft' 
838241     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [219] goal: 5342, source line: 308, command: 'rule andLeft' 
838242     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [220] goal: 5343, source line: 309, command: 'rule ifthenelse_split occ=0' 
838243     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [221] goal: 5344, source line: 310, command: 'rule getOfSwap' 
838244     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [222] goal: 5346, source line: 311, command: 'rule ifthenelse_negated' 
838244     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [223] goal: 5347, source line: 312, command: 'rule ifthenelse_split occ=0' 
838245     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [224] goal: 5348, source line: 313, command: 'rule andLeft' 
838246     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [225] goal: 5350, source line: 314, command: 'rule andLeft' 
838247     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [226] goal: 5351, source line: 315, command: 'rule andLeft' 
838247     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [227] goal: 5352, source line: 316, command: 'rule ifthenelse_split occ=0' 
838248     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [228] goal: 5353, source line: 317, command: 'tryclose branch' 
838357     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [229] goal: 5354, source line: 318, command: 'rule ifthenelse_split occ=0' 
838358     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [230] goal: 5463, source line: 319, command: 'tryclose branch' 
838365     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [231] goal: 5464, source line: 320, command: 'tryclose branch' 
838479     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [232] goal: 5349, source line: 321, command: 'tryclose branch' 
838650     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [233] goal: 5345, source line: 322, command: 'rule ifthenelse_split' 
838652     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [234] goal: 5660, source line: 324, command: 'rule getOfSwap' 
838653     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [235] goal: 5662, source line: 325, command: 'rule ifthenelse_negated' 
838654     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [236] goal: 5663, source line: 326, command: 'rule ifthenelse_split occ=0' 
838655     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [237] goal: 5664, source line: 327, command: 'rule andLeft' 
838655     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [238] goal: 5666, source line: 328, command: 'rule andLeft' 
838656     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [239] goal: 5667, source line: 329, command: 'rule andLeft' 
838656     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [240] goal: 5668, source line: 330, command: 'rule ifthenelse_split occ=0' 
838657     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [241] goal: 5669, source line: 331, command: 'tryclose branch' 
838772     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [242] goal: 5670, source line: 332, command: 'tryclose branch' 
838780     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [243] goal: 5665, source line: 333, command: 'tryclose branch' 
838892     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [244] goal: 5661, source line: 334, command: 'rule getOfSwap' 
838893     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [245] goal: 5887, source line: 336, command: 'rule ifthenelse_negated' 
838894     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [246] goal: 5888, source line: 337, command: 'rule ifthenelse_split occ=0' 
838895     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [247] goal: 5889, source line: 338, command: 'rule andLeft' 
838896     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [248] goal: 5891, source line: 339, command: 'rule andLeft' 
838896     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [249] goal: 5892, source line: 340, command: 'rule andLeft' 
838896     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [250] goal: 5893, source line: 341, command: 'rule ifthenelse_split occ=0' 
838897     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [251] goal: 5894, source line: 342, command: 'tryclose branch' 
838903     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [252] goal: 5895, source line: 343, command: 'rule ifthenelse_split occ=0' 
838904     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [253] goal: 5897, source line: 344, command: 'tryclose branch' 
838997     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [254] goal: 5898, source line: 345, command: 'tryclose branch' 
839004     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [255] goal: 5890, source line: 346, command: 'tryclose branch' 
839010     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [256] goal: 5340, source line: 347, command: 'tryclose branch' 
839135     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [257] goal: 4954, source line: 348, command: 'rule getOfSwap' 
839135     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [258] goal: 6115, source line: 350, command: 'rule ifthenelse_negated' 
839136     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [259] goal: 6116, source line: 351, command: 'rule ifthenelse_split occ=0' 
839137     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [260] goal: 6117, source line: 352, command: 'rule andLeft' 
839138     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [261] goal: 6119, source line: 353, command: 'rule andLeft' 
839138     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [262] goal: 6120, source line: 354, command: 'rule andLeft' 
839139     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [263] goal: 6121, source line: 355, command: 'rule ifthenelse_split occ=0' 
839139     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [264] goal: 6122, source line: 356, command: 'tryclose branch' 
839211     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [265] goal: 6123, source line: 357, command: 'rule ifthenelse_split occ=0' 
839212     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [266] goal: 6193, source line: 358, command: 'rule getOfSwap' 
839213     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [267] goal: 6195, source line: 359, command: 'rule ifthenelse_negated' 
839213     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [268] goal: 6196, source line: 360, command: 'rule ifthenelse_split occ=0' 
839214     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [269] goal: 6197, source line: 361, command: 'tryclose branch' 
839221     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [270] goal: 6198, source line: 362, command: 'tryclose branch' 
839227     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [271] goal: 6194, source line: 363, command: 'tryclose branch' 
839381     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [272] goal: 6118, source line: 364, command: 'tryclose branch' 
839492     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [273] goal: 4952, source line: 365, command: 'rule getOfSwap' 
839492     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [274] goal: 6456, source line: 367, command: 'rule ifthenelse_negated' 
839493     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [275] goal: 6457, source line: 368, command: 'rule ifthenelse_split occ=0' 
839494     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [276] goal: 6458, source line: 369, command: 'tryclose branch' 
839712     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [277] goal: 6459, source line: 370, command: 'tryclose branch' 
839819     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [278] goal: 4949, source line: 371, command: 'cut 'int::seqGet(s_0, v_y_0)=v_x_0'' 
839819     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [279] goal: 6735, source line: 375, command: 'tryclose branch' 
843643     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [280] goal: 6735, source line: 378, command: 'rule seqNPermSwapNPerm' 
843648     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [281] goal: 8783, source line: 380, command: 'instantiate hide var=iv with='jv_1'' 
843649     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'' 
843650     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [283] goal: 8785, source line: 382, command: 'rule impLeft' 
843651     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [284] goal: 8786, source line: 383, command: 'tryclose branch' 
843812     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))'' 
843812     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [286] goal: 8909, source line: 385, command: 'instantiate hide var=iv with='jv_1'' 
843813     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'' 
843814     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [288] goal: 8911, source line: 387, command: 'rule impLeft' 
843815     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [289] goal: 8912, source line: 388, command: 'tryclose branch' 
843955     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [290] goal: 8913, source line: 389, command: 'tryclose branch' 
847644     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [291] goal: 6736, source line: 390, command: 'tryclose branch' 
851470     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [292] goal: 6736, source line: 397, command: 'rule seqNPermSwapNPerm formula='seqNPerm(s_0)'' 
851475     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'' 
851476     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [294] goal: 12634, source line: 400, command: 'instantiate hide var=jv with='jv_0'' 
851477     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [295] goal: 12635, source line: 401, command: 'rule impLeft' 
851478     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [296] goal: 12636, source line: 402, command: 'tryclose branch' 
851617     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))'' 
851618     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'' 
851619     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [299] goal: 12758, source line: 405, command: 'instantiate hide var=jv with='jv_1'' 
851620     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)' ...' 
851621     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [301] goal: 12760, source line: 407, command: 'tryclose branch' 
853033     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm2/Taclet_schiffl_thm_1.proof 
853033     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 106.4ns 
853034     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
856280     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.25s 
856280     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: schiffl_thm_1 
857341     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: schiffl_thm_1 
857343     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 8ns 
857343     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [1] goal: 0, source line: 50, command: 'macro split-prop' 
857353     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)'' 
857363     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [3] goal: 11, source line: 52, command: 'instantiate hide var=x with='f_x'' 
857365     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [4] goal: 12, source line: 53, command: 'instantiate hide var=y with='f_y'' 
857368     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [5] goal: 13, source line: 54, command: 'rule impLeft' 
857369     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [6] goal: 14, source line: 55, command: 'tryclose branch' 
857375     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [7] goal: 15, source line: 56, command: 'rule exLeft' 
857376     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [8] goal: 23, source line: 57, command: 'macro split-prop' 
857381     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [9] goal: 27, source line: 58, command: 'rule seqPermDef occ=1' 
857382     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [10] goal: 28, source line: 59, command: 'rule andRight' 
857384     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [11] goal: 29, source line: 60, command: 'tryclose branch' 
857396     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [12] goal: 30, source line: 61, command: 'instantiate hide var=s with='r_0'' 
857396     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [13] goal: 46, source line: 62, command: 'rule andRight' 
857398     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [14] goal: 47, source line: 63, command: 'tryclose branch' 
857457     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [15] goal: 48, source line: 64, command: 'rule allRight' 
857458     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [16] goal: 119, source line: 65, command: 'rule impRight' 
857458     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [17] goal: 120, source line: 66, command: 'instantiate hide var=iv with='iv_0'' 
857459     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [18] goal: 121, source line: 67, command: 'rule impLeft' 
857460     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [19] goal: 122, source line: 68, command: 'tryclose branch' 
857533     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [20] goal: 123, source line: 69, command: 'rule andLeft' 
857534     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [21] goal: 203, source line: 70, command: 'rule seqNPermRange' 
857534     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [22] goal: 204, source line: 71, command: 'instantiate hide var=iv with='iv_0'' 
857535     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [23] goal: 205, source line: 72, command: 'rule impLeft' 
857536     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [24] goal: 206, source line: 73, command: 'tryclose branch' 
857540     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [25] goal: 207, source line: 74, command: 'rule andLeft' 
857541     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [26] goal: 215, source line: 75, command: 'rule andLeft' 
857541     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [27] goal: 216, source line: 76, command: 'rule seqNPermRange' 
857541     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [28] goal: 217, source line: 77, command: 'instantiate hide var=iv with='f_x'' 
857542     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [29] goal: 218, source line: 78, command: 'rule impLeft' 
857543     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [30] goal: 219, source line: 79, command: 'tryclose branch' 
857638     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [31] goal: 220, source line: 80, command: 'rule andLeft' 
857638     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [32] goal: 311, source line: 81, command: 'rule andLeft' 
857639     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [33] goal: 312, source line: 82, command: 'rule seqNPermRange' 
857640     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [34] goal: 313, source line: 83, command: 'instantiate hide var=iv with='f_y'' 
857641     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [35] goal: 314, source line: 84, command: 'rule impLeft' 
857642     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [36] goal: 315, source line: 85, command: 'tryclose branch' 
857738     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [37] goal: 316, source line: 86, command: 'rule andLeft' 
857739     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [38] goal: 410, source line: 87, command: 'rule andLeft' 
857739     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [39] goal: 411, source line: 88, command: 'rule getOfSeqDef occ=0' 
857740     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [40] goal: 412, source line: 89, command: 'rule getOfSeqDef' 
857741     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [41] goal: 413, source line: 90, command: 'rule ifthenelse_split occ=0' 
857742     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [42] goal: 414, source line: 91, command: 'rule andLeft occ=0' 
857742     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [43] goal: 416, source line: 92, command: 'rule sub_zero_2 occ=0' 
857742     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [44] goal: 417, source line: 93, command: 'rule ifthenelse_split occ=2' 
857743     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [45] goal: 418, source line: 94, command: 'rule andLeft' 
857744     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [46] goal: 420, source line: 95, command: 'rule sub_zero_2 occ=0' 
857744     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [47] goal: 421, source line: 96, command: 'rule add_zero_right occ=0' 
857744     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [48] goal: 422, source line: 97, command: 'rule add_zero_right occ=0' 
857745     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [49] goal: 423, source line: 98, command: 'rule add_zero_right occ=0' 
857745     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [50] goal: 424, source line: 99, command: 'rule add_zero_right occ=0' 
857746     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [51] goal: 425, source line: 100, command: 'rule add_zero_right occ=0' 
857746     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [52] goal: 426, source line: 101, command: 'rule add_zero_right occ=0' 
857747     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [53] goal: 427, source line: 102, command: 'rule ifthenelse_split occ=0' 
857747     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [54] goal: 428, source line: 103, command: 'rule ifthenelse_split occ=0' 
857748     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [55] goal: 430, source line: 104, command: 'tryclose branch' 
857751     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [56] goal: 431, source line: 105, command: 'tryclose branch' 
857794     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [57] goal: 429, source line: 106, command: 'rule ifthenelse_split occ=0' 
857795     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [58] goal: 473, source line: 107, command: 'tryclose branch' 
857864     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [59] goal: 474, source line: 108, command: 'rule ifthenelse_split occ=0' 
857865     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [60] goal: 541, source line: 109, command: 'rule seqNPermInjective' 
857866     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [61] goal: 543, source line: 110, command: 'instantiate hide var=iv with='iv_0'' 
857867     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [62] goal: 544, source line: 111, command: 'instantiate hide var=jv with='f_y'' 
857868     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [63] goal: 545, source line: 112, command: 'rule impLeft' 
857869     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [64] goal: 546, source line: 113, command: 'tryclose branch' 
857923     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [65] goal: 547, source line: 114, command: 'tryclose branch' 
857926     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [66] goal: 542, source line: 115, command: 'rule ifthenelse_split occ=0' 
857927     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [67] goal: 606, source line: 116, command: 'rule seqNPermInjective' 
857928     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [68] goal: 608, source line: 117, command: 'instantiate hide var=iv with='iv_0'' 
857929     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [69] goal: 609, source line: 118, command: 'instantiate hide var=jv with='f_x'' 
857930     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [70] goal: 610, source line: 119, command: 'rule impLeft' 
857930     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [71] goal: 611, source line: 120, command: 'tryclose branch' 
857986     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [72] goal: 612, source line: 121, command: 'tryclose branch' 
857989     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [73] goal: 607, source line: 122, command: 'tryclose branch' 
857992     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [74] goal: 419, source line: 123, command: 'tryclose branch' 
858062     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [75] goal: 415, source line: 124, command: 'tryclose branch' 
858133     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_eqSameSeq.proof 
858133     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 124.6ns 
858134     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
861451     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.32s 
861451     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: eqSameSeq 
862535     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: eqSameSeq 
862556     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 18.04ms