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

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

tests
0

failures
0

ignored
10m20.76s

duration
100%

successful

Tests

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

Standard output

569        INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src/test/resources/testcase/dummyTrue.key 
592        DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 7.89ms 
799        INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
831        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)

1759       DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for Meta 
1762       DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for Meta 
1768       DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for Meta 
1768       DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for Meta 
3134       DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for JavaBigintExpression 
8179       DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 7.38s 
8242       INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof dummyTrue.key 
8273       DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 33.6ns 
8286       INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/firstOrder/Taclet_eqTermCut.proof 
8286       DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 520.69ns 
8290       INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
10932      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.64s 
10934      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: eqTermCut 
11843      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: eqTermCut 
11865      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 17.14ms 
11880      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/firstOrder/Taclet_equivAllRight.proof 
11880      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 197.7ns 
11882      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
14420      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.54s 
14425      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: equivAllRight 
15246      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: equivAllRight 
15262      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 9.21ms 
15265      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_irrflConcrete1.proof 
15265      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 368.6ns 
15267      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
17815      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.55s 
17816      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: irrflConcrete1 
18668      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: irrflConcrete1 
18684      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 11.19ms 
18687      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_irrflConcrete2.proof 
18688      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 368ns 
18689      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
21068      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.38s 
21068      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: irrflConcrete2 
21858      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: irrflConcrete2 
21863      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.27ms 
21866      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_cancel_gtPos.proof 
21867      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 486.39ns 
21868      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
24222      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.35s 
24222      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: cancel_gtPos 
25034      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: cancel_gtPos 
25072      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 34.06ms 
25074      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_cancel_gtNeg.proof 
25074      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 162.7ns 
25075      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
27397      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.32s 
27397      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: cancel_gtNeg 
28188      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: cancel_gtNeg 
28206      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 15.32ms 
28208      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intRulesIgnoringOF/Taclet_moduloIntIsInInt.proof 
28208      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 117.9ns 
28209      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
30601      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.39s 
30601      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: moduloIntIsInInt 
31388      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: moduloIntIsInInt 
31391      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 723.59ns 
31392      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intRulesIgnoringOF/Taclet_moduloLongIsInLong.proof 
31393      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 237.9ns 
31393      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
33722      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.33s 
33722      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: moduloLongIsInLong 
34479      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: moduloLongIsInLong 
34482      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 569.29ns 
34488      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intRulesIgnoringOF/Taclet_moduloShortIsInShort.proof 
34488      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 235.2ns 
34489      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
36822      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.33s 
36822      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: moduloShortIsInShort 
37764      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: moduloShortIsInShort 
37768      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.98ms 
37773      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intRulesIgnoringOF/Taclet_moduloByteIsInByte.proof 
37773      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 137.6ns 
37775      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
40111      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.34s 
40111      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: moduloByteIsInByte 
40874      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: moduloByteIsInByte 
40877      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 577.59ns 
40889      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intRulesIgnoringOF/Taclet_moduloCharIsInChar.proof 
40890      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 625.09ns 
40891      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
43250      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.36s 
43251      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: moduloCharIsInChar 
44003      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: moduloCharIsInChar 
44005      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 605.89ns 
44007      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_div_unique1.proof 
44007      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 132.3ns 
44008      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
46301      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.29s 
46301      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: div_unique1 
47056      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: div_unique1 
47092      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 31.86ms 
47093      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_div_unique2.proof 
47094      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 131.4ns 
47094      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
49399      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.3s 
49400      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: div_unique2 
50131      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: div_unique2 
50160      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 26.36ms 
50162      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_div_exists.proof 
50162      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 138.7ns 
50163      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
52463      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.3s 
52463      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: div_exists 
53194      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: div_exists 
53395      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 192.05ms 
53399      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_div_one.proof 
53400      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 357.5ns 
53401      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
55712      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.31s 
55713      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: div_one 
56467      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: div_one 
56476      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.69ms 
56479      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdiv_one.proof 
56480      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 381ns 
56481      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
58785      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.3s 
58786      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdiv_one 
59544      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdiv_one 
59547      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.17ms 
59550      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_div_zero.proof 
59550      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 325.8ns 
59551      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
61835      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.28s 
61836      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: div_zero 
62622      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: div_zero 
62680      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 51.48ms 
62683      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divResZero1.proof 
62683      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 131.6ns 
62684      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
64986      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.3s 
64987      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divResZero1 
65803      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divResZero1 
65816      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 9.38ms 
65818      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divResZero2.proof 
65819      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 333.1ns 
65820      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
68155      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.34s 
68156      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divResZero2 
68887      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divResZero2 
68898      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 8.01ms 
68901      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divResOne1.proof 
68901      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 341.6ns 
68902      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
71219      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.32s 
71220      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divResOne1 
71954      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divResOne1 
71966      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 8.97ms 
71969      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divResOne2.proof 
71969      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 319.9ns 
71970      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
74268      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.3s 
74269      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divResOne2 
75022      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divResOne2 
75043      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 17.9ms 
75049      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_div_cancel1.proof 
75050      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 127.8ns 
75050      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
77339      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.29s 
77340      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: div_cancel1 
78086      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: div_cancel1 
78110      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 20.75ms 
78113      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_div_cancel2.proof 
78113      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 325.7ns 
78114      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
80399      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.28s 
80399      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: div_cancel2 
81148      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: div_cancel2 
81151      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.21ms 
81153      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divAddMultDenom.proof 
81154      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 292.3ns 
81155      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
83427      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.27s 
83427      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divAddMultDenom 
84182      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divAddMultDenom 
84212      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 24.47ms 
84213      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divMinus.proof 
84213      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 130.8ns 
84214      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
86522      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.31s 
86523      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divMinus 
87251      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divMinus 
87294      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 36.03ms 
87295      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divMinusDenom.proof 
87295      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 99.7ns 
87296      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
89588      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.29s 
89588      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divMinusDenom 
90314      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divMinusDenom 
90343      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 24.06ms 
90345      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divLeastDPos.proof 
90345      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 115.3ns 
90346      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
92652      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.31s 
92654      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divLeastDPos 
93406      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divLeastDPos 
93419      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 9.79ms 
93420      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divLeastDNeg.proof 
93420      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 115.3ns 
93421      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
95699      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.28s 
95699      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divLeastDNeg 
96443      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divLeastDNeg 
96454      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 8.19ms 
96455      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divGreatestDPos.proof 
96455      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 92.4ns 
96456      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
98727      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.27s 
98727      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divGreatestDPos 
99473      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divGreatestDPos 
99482      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 6.92ms 
99484      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divGreatestDNeg.proof 
99485      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 315.89ns 
99486      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
101754     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.27s 
101754     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divGreatestDNeg 
102498     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divGreatestDNeg 
102504     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.22ms 
102506     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divIncreasingPos.proof 
102506     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 86.5ns 
102507     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
104789     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.28s 
104789     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divIncreasingPos 
105516     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divIncreasingPos 
105522     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.93ms 
105524     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divIncreasingNeg.proof 
105525     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 316ns 
105526     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
107811     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.29s 
107812     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divIncreasingNeg 
108537     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divIncreasingNeg 
108543     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.04ms 
108544     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdiv_zero.proof 
108544     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 88.6ns 
108545     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
110831     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.29s 
110831     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdiv_zero 
111574     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdiv_zero 
111577     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.23ms 
111578     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdivPulloutMinusNum.proof 
111578     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 84.9ns 
111579     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
113857     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.28s 
113857     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdivPulloutMinusNum 
114599     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdivPulloutMinusNum 
114608     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 6.39ms 
114609     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdivPulloutMinusDenom.proof 
114610     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 107.1ns 
114610     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
116882     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.27s 
116883     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdivPulloutMinusDenom 
117634     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdivPulloutMinusDenom 
117681     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 39.45ms 
117684     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdiv_uniquePosPos.proof 
117684     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 298.4ns 
117685     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
120022     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.34s 
120022     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdiv_uniquePosPos 
120766     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdiv_uniquePosPos 
120780     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 11.02ms 
120781     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdiv_uniquePosNeg.proof 
120781     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 93.3ns 
120782     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
123042     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.26s 
123042     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdiv_uniquePosNeg 
123789     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdiv_uniquePosNeg 
123803     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 10.65ms 
123804     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdiv_uniqueNegPos.proof 
123804     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 87ns 
123805     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
126086     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.28s 
126086     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdiv_uniqueNegPos 
126810     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdiv_uniqueNegPos 
126823     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 10.91ms 
126825     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdiv_uniqueNegNeg.proof 
126825     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 94.8ns 
126826     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
129111     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.28s 
129111     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdiv_uniqueNegNeg 
129853     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdiv_uniqueNegNeg 
129867     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 10.46ms 
129868     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdivMultDenom1.proof 
129868     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 90.6ns 
129869     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
132139     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.27s 
132139     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdivMultDenom1 
132885     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdivMultDenom1 
132917     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 27.34ms 
132919     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdivMultDenom2.proof 
132919     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 153.9ns 
132920     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
135193     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.27s 
135193     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdivMultDenom2 
135949     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdivMultDenom2 
135951     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 849.89ns 
135953     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_mod_geZero.proof 
135953     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 152.2ns 
135954     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
138238     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.28s 
138238     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: mod_geZero 
138984     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: mod_geZero 
138987     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.85ms 
138989     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_mod_lessDenom.proof 
138989     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 147.7ns 
138990     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
141264     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.27s 
141264     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: mod_lessDenom 
142008     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: mod_lessDenom 
142015     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.63ms 
142016     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmod_NumPos.proof 
142016     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 78.9ns 
142017     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
144298     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.28s 
144299     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmod_NumPos 
145021     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmod_NumPos 
145028     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.58ms 
145029     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmod_NumNeg.proof 
145029     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 71.7ns 
145030     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
147308     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.28s 
147308     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmod_NumNeg 
148056     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmod_NumNeg 
148072     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 12.56ms 
148074     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmod_geZero.proof 
148075     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 604.09ns 
148076     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
150340     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.26s 
150341     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmod_geZero 
151088     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmod_geZero 
151095     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.7ms 
151097     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmodNumZero.proof 
151097     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 252.8ns 
151098     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
153355     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.26s 
153355     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmodNumZero 
154103     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmodNumZero 
154106     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.06ms 
154108     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmod_pulloutminusNum.proof 
154109     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 250.4ns 
154110     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
156378     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.27s 
156379     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmod_pulloutminusNum 
157130     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmod_pulloutminusNum 
157133     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.38ms 
157134     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmod_pulloutminusDenom.proof 
157134     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 72.5ns 
157135     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
159391     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.26s 
159391     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmod_pulloutminusDenom 
160132     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmod_pulloutminusDenom 
160135     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.49ms 
160136     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmodUnique1.proof 
160136     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 68.6ns 
160137     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
162423     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.29s 
162423     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmodUnique1 
163146     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmodUnique1 
163198     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 43.35ms 
163200     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmodUnique2.proof 
163201     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 280.3ns 
163202     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
165486     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.28s 
165486     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmodUnique2 
166208     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmodUnique2 
166307     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 90.06ms 
166313     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_intDivRem.proof 
166313     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 300.9ns 
166314     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
168580     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.27s 
168580     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: intDivRem 
169327     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: intDivRem 
169333     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.99ms 
169335     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmodjmod.proof 
169336     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 254.3ns 
169337     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
171617     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.28s 
171617     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmodjmod 
172357     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmodjmod 
172385     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 23.8ms 
172387     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmodDivisible.proof 
172388     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 359.2ns 
172389     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
174650     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.26s 
174650     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmodDivisible 
175396     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmodDivisible 
175416     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 16.91ms 
175417     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmodDivisibleRep.proof 
175417     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 76.6ns 
175418     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
177677     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.26s 
177677     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmodDivisibleRep 
178417     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmodDivisibleRep 
178419     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 933.09ns 
178421     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdivAddMultDenom.proof 
178422     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 228.6ns 
178423     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
180690     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.27s 
180691     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdivAddMultDenom 
181414     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdivAddMultDenom 
181513     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 88.09ms 
181516     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmodAltZero.proof 
181516     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 250.1ns 
181517     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
183811     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.29s 
183811     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmodAltZero 
184555     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmodAltZero 
184563     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 5.96ms 
184565     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmodAddMultDenomZero.proof 
184565     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 70.4ns 
184565     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
186823     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.26s 
186823     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmodAddMultDenomZero 
187563     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmodAddMultDenomZero 
187569     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.16ms 
187570     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_polyDiv_zero.proof 
187570     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 60.5ns 
187571     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
189834     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.26s 
189835     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: polyDiv_zero 
190574     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: polyDiv_zero 
190587     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 10.5ms 
190589     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_polyMod_ltdivDenom.proof 
190589     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 79.6ns 
190589     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
192847     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.26s 
192847     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: polyMod_ltdivDenom 
193585     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: polyMod_ltdivDenom 
193595     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.48ms 
193597     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_empty.proof 
193597     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 62.2ns 
193597     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
195854     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.26s 
195854     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_empty 
196603     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_empty 
196606     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.31ms 
196608     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_induction_upper.proof 
196608     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 108ns 
196609     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
198884     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.27s 
198884     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_upper 
199606     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_induction_upper 
199618     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 10.64ms 
199619     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_induction_lower.proof 
199619     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 71.8ns 
199620     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
201902     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.28s 
201902     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_lower 
202622     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_induction_lower 
202635     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 10.03ms 
202636     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_bounds.proof 
202636     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 63.6ns 
202637     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
204908     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.27s 
204909     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_bounds 
205652     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_bounds 
205663     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 8.04ms 
205664     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_bounds2.proof 
205664     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 63.2ns 
205665     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
207924     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.26s 
207924     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_bounds2 
208667     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_bounds2 
208678     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 8.31ms 
208679     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_induction_upper2.proof 
208679     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 67.8ns 
208680     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
210927     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.25s 
210927     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_upper2 
211667     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_induction_upper2 
211670     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 877.19ns 
211674     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_induction_upper_concrete.proof 
211674     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 75.2ns 
211675     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
213929     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.25s 
213929     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_upper_concrete 
214669     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_induction_upper_concrete 
214672     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.38ms 
214673     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_induction_upper_concrete_2.proof 
214673     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 80.2ns 
214674     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
216943     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.27s 
216943     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_upper_concrete_2 
217666     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_induction_upper_concrete_2 
217671     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.91ms 
217672     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_induction_upper2_concrete.proof 
217673     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 77.6ns 
217673     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
219957     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.28s 
219957     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_upper2_concrete 
220677     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_induction_upper2_concrete 
220679     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 776.09ns 
220680     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_induction_lower_concrete.proof 
220680     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 67.7ns 
220681     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
222948     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.27s 
222948     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_lower_concrete 
223686     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_induction_lower_concrete 
223688     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 451.39ns 
223689     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_induction_lower2.proof 
223689     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 62.3ns 
223690     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
225945     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.25s 
225945     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_lower2 
226684     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_induction_lower2 
226688     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.56ms 
226689     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_induction_lower2_concrete.proof 
226689     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 59.1ns 
226690     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
228944     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.25s 
228944     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_lower2_concrete 
229685     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_induction_lower2_concrete 
229687     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 599.79ns 
229689     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_positive.proof 
229689     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 62.5ns 
229689     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
231941     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.25s 
231941     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_positive 
232683     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_positive 
232715     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 28.96ms 
232716     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_upper_bound.proof 
232716     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 72.6ns 
232717     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
234969     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.25s 
234969     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_upper_bound 
235709     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_upper_bound 
235744     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 31.65ms 
235745     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_lower_bound.proof 
235745     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 75.4ns 
235746     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
238033     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.29s 
238033     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_lower_bound 
238756     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_lower_bound 
238776     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 17.52ms 
238778     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_positive_lower_bound_element.proof 
238778     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 67.7ns 
238778     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
241077     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.3s 
241077     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_positive_lower_bound_element 
241819     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_positive_lower_bound_element 
241848     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 24.6ms 
241849     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_sub_same_index.proof 
241849     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 73.4ns 
241850     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
244115     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.27s 
244115     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_sub_same_index 
244857     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_sub_same_index 
244876     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 16.02ms 
244878     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_less_same_index.proof 
244878     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 195ns 
244879     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
247158     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.28s 
247158     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_less_same_index 
247901     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_less_same_index 
247934     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 27.66ms 
247935     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_equal_except_one_index.proof 
247935     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 72.4ns 
247936     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
250192     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.26s 
250192     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_equal_except_one_index 
250936     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_equal_except_one_index 
250952     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 12.65ms 
250953     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_is_max.proof 
250953     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 77.2ns 
250954     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
253215     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.26s 
253215     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_is_max 
253955     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_is_max 
253968     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 9.53ms 
253969     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_is_max2.proof 
253969     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 70ns 
253970     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
256261     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.29s 
256261     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_is_max2 
256983     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_is_max2 
256997     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 11.16ms 
256998     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_is_max3.proof 
256998     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 72.4ns 
256999     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
259279     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.28s 
259279     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_is_max3 
260026     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_is_max3 
260039     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 9.33ms 
260041     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_is_max4.proof 
260041     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 194.7ns 
260042     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
262301     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.26s 
262301     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_is_max4 
263047     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_is_max4 
263064     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 13.93ms 
263066     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_lt_max.proof 
263066     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 63.8ns 
263066     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
265325     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.26s 
265325     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_lt_max 
266067     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_lt_max 
266082     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 11.6ms 
266083     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_lt_max2.proof 
266083     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 74.6ns 
266084     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
268340     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.26s 
268340     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_lt_max2 
269102     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_lt_max2 
269117     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 12.03ms 
269118     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_lt_max3.proof 
269118     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 74ns 
269119     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
271372     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.25s 
271372     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_lt_max3 
272112     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_lt_max3 
272127     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 11.44ms 
272129     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_lt_max4.proof 
272130     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 226.4ns 
272131     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
274417     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.29s 
274417     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_lt_max4 
275139     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_lt_max4 
275152     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 10.5ms 
275153     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_gt0.proof 
275153     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 64ns 
275154     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
277434     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.28s 
277434     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_gt0 
278175     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_gt0 
278188     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 10.82ms 
278189     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_gt0_alt.proof 
278190     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 68.3ns 
278190     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
280453     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.26s 
280453     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_gt0_alt 
281196     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_gt0_alt 
281210     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 11.76ms 
281212     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_add_concrete.proof 
281212     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 76ns 
281212     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
283466     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.25s 
283466     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_add_concrete 
284206     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_add_concrete 
284211     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.38ms 
284212     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bprod/Taclet_bprod_all_positive.proof 
284212     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 58.9ns 
284213     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
286464     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.25s 
286464     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bprod_all_positive 
287204     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bprod_all_positive 
287214     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 7.73ms 
287215     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bprod/Taclet_bprod_split.proof 
287215     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 61.4ns 
287216     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
289465     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.25s 
289466     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bprod_split 
290206     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bprod_split 
290209     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.46ms 
290210     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powConcrete0.proof 
290210     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 59ns 
290211     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
292477     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.27s 
292477     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powConcrete0 
293198     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powConcrete0 
293200     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 516.19ns 
293201     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powConcrete1.proof 
293201     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 59.3ns 
293202     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
295478     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.28s 
295478     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powConcrete1 
296221     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powConcrete1 
296224     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 616.39ns 
296225     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powSplitFactor.proof 
296225     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 55.9ns 
296225     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
298477     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.25s 
298477     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powSplitFactor 
299219     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powSplitFactor 
299224     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.83ms 
299225     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powAdd.proof 
299225     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 68.7ns 
299226     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
301477     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.25s 
301477     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powAdd 
302218     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powAdd 
302223     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.81ms 
302225     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powMono.proof 
302225     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 188.6ns 
302226     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
304481     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.26s 
304481     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powMono 
305221     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powMono 
305230     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 6.74ms 
305231     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powMonoConcrete.proof 
305231     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 61.6ns 
305232     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
307490     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.26s 
307491     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powMonoConcrete 
308235     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powMonoConcrete 
308239     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.58ms 
308240     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powMonoConcreteRight.proof 
308240     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 56.7ns 
308240     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
310521     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.28s 
310521     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powMonoConcreteRight 
311242     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powMonoConcreteRight 
311244     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 389.89ns 
311245     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powPositive.proof 
311245     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 61.3ns 
311246     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
313528     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.28s 
313529     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powPositive 
314252     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powPositive 
314257     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.51ms 
314258     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powPositiveConcrete.proof 
314258     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 65.1ns 
314259     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
316544     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.29s 
316544     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powPositiveConcrete 
317285     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powPositiveConcrete 
317287     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 510.29ns 
317288     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powGeq1Concrete.proof 
317288     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 50.6ns 
317289     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
319546     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.26s 
319546     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powGeq1Concrete 
320295     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powGeq1Concrete 
320297     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 469.89ns 
320298     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_pow2InIntLower.proof 
320298     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 90.1ns 
320299     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
322545     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.25s 
322545     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: pow2InIntLower 
323286     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: pow2InIntLower 
323288     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 462.59ns 
323290     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_pow2InIntUpper.proof 
323290     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 172.5ns 
323291     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
325542     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.25s 
325542     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: pow2InIntUpper 
326284     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: pow2InIntUpper 
326287     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.65ms 
326288     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logSelfConcrete.proof 
326289     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 108.1ns 
326289     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
328552     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.26s 
328552     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logSelfConcrete 
329272     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logSelfConcrete 
329278     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.45ms 
329280     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_log1Concrete.proof 
329280     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 64.4ns 
329280     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
331562     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.28s 
331562     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: log1Concrete 
332282     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: log1Concrete 
332285     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.43ms 
332286     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logProduct.proof 
332286     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 50.7ns 
332287     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
334555     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.27s 
334556     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logProduct 
335295     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logProduct 
335300     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.14ms 
335301     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logTimesBaseConcrete.proof 
335301     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 52.3ns 
335302     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
337553     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.25s 
337553     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logTimesBaseConcrete 
338294     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logTimesBaseConcrete 
338297     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.84ms 
338298     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logProdIdentity.proof 
338298     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 62.6ns 
338299     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
340552     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.25s 
340552     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logProdIdentity 
341299     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logProdIdentity 
341311     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 8.42ms 
341313     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logProdIdentityConcrete.proof 
341313     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 176.8ns 
341317     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
343566     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.25s 
343566     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logProdIdentityConcrete 
344305     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logProdIdentityConcrete 
344308     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.48ms 
344310     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logPowIdentity.proof 
344310     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 51.8ns 
344310     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
346553     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.24s 
346553     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logPowIdentity 
347292     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logPowIdentity 
347295     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 979.29ns 
347296     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logPowIdentityConcrete.proof 
347296     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 57.6ns 
347296     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
349563     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.27s 
349563     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logPowIdentityConcrete 
350282     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logPowIdentityConcrete 
350286     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.5ms 
350287     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logPositive.proof 
350287     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 60.4ns 
350288     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
352550     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.26s 
352550     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logPositive 
353294     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logPositive 
353311     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 14.29ms 
353312     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logPositiveConcrete.proof 
353313     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 997.59ns 
353314     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
355569     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.25s 
355569     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logPositiveConcrete 
356309     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logPositiveConcrete 
356312     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 317ns 
356314     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logMono.proof 
356314     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 59.8ns 
356315     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
358564     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.25s 
358564     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logMono 
359304     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logMono 
359328     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 20.7ms 
359330     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logMonoConcrete.proof 
359330     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 65.7ns 
359331     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
361582     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.25s 
361582     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logMonoConcrete 
362323     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logMonoConcrete 
362326     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.26ms 
362327     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powLogLess.proof 
362328     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 52.4ns 
362328     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
364583     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.25s 
364583     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powLogLess 
365323     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powLogLess 
365337     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 11.55ms 
365339     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powLogMore2.proof 
365339     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 69.7ns 
365339     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
367611     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.27s 
367611     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powLogMore2 
368332     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powLogMore2 
368345     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 10.54ms 
368346     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logLessThanPow.proof 
368346     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 73ns 
368347     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
370624     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.28s 
370624     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logLessThanPow 
371367     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logLessThanPow 
371383     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 13.59ms 
371385     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logLessThanPowConcrete.proof 
371385     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 67.6ns 
371385     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
373650     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.26s 
373650     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logLessThanPowConcrete 
374395     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logLessThanPowConcrete 
374398     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 447.69ns 
374401     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logSqueeze.proof 
374401     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 73.9ns 
374402     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
376652     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.25s 
376652     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logSqueeze 
377397     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logSqueeze 
377401     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.83ms 
377402     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/booleanRules/Taclet_ifthenelse_equals.proof 
377402     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 60.6ns 
377403     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
379674     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.27s 
379674     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: ifthenelse_equals 
380400     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: ifthenelse_equals 
380403     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.23ms 
380404     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/booleanRules/Taclet_ifthenelse_equals_1.proof 
380404     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 57.6ns 
380405     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
382673     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.27s 
382673     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: ifthenelse_equals_1 
383396     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: ifthenelse_equals_1 
383398     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 650.89ns 
383399     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/booleanRules/Taclet_ifthenelse_equals_2.proof 
383399     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 50.9ns 
383400     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
385665     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.26s 
385665     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: ifthenelse_equals_2 
386408     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: ifthenelse_equals_2 
386410     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 646.99ns 
386418     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/locSet/Taclet_disjointWithSingleton1.proof 
386418     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 65.6ns 
386419     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
388681     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.26s 
388681     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: disjointWithSingleton1 
389427     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: disjointWithSingleton1 
389429     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.27ms 
389431     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/locSet/Taclet_disjointWithSingleton2.proof 
389431     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 48.8ns 
389431     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
391678     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.25s 
391678     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: disjointWithSingleton2 
392420     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: disjointWithSingleton2 
392423     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.12ms 
392424     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/locSet/Taclet_disjointArrayRanges.proof 
392424     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 60ns 
392425     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
394692     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.27s 
394692     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: disjointArrayRanges 
395415     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: disjointArrayRanges 
395422     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 5.32ms 
395424     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/locSet/Taclet_disjointArrayRangeAllFields1.proof 
395424     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 58.4ns 
395425     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
397691     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.27s 
397691     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: disjointArrayRangeAllFields1 
398435     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: disjointArrayRangeAllFields1 
398442     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.39ms 
398445     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/locSet/Taclet_disjointArrayRangeAllFields2.proof 
398445     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 181.2ns 
398445     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
400691     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.25s 
400691     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: disjointArrayRangeAllFields2 
401436     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: disjointArrayRangeAllFields2 
401442     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.4ms 
401443     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqSelfDefinition.proof 
401443     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 70.7ns 
401444     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
403709     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.27s 
403709     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqSelfDefinition 
404439     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqSelfDefinition 
404446     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.83ms 
404447     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqOutsideValue.proof 
404447     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 65.5ns 
404448     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
406718     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.27s 
406718     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqOutsideValue 
407468     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqOutsideValue 
407472     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.11ms 
407473     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_castedGetAny.proof 
407473     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 60.3ns 
407474     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
409723     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.25s 
409723     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: castedGetAny 
410472     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: castedGetAny 
410476     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.04ms 
410477     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqGetAlphaCast.proof 
410477     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 57.6ns 
410478     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
412742     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.26s 
412742     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqGetAlphaCast 
413473     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqGetAlphaCast 
413475     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 637.19ns 
413476     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqSingleton.proof 
413477     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 56.9ns 
413477     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
415741     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.26s 
415741     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqSingleton 
416489     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqSingleton 
416492     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 843.19ns 
416493     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqSingletonConcrete.proof 
416493     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 68.1ns 
416494     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
418739     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.25s 
418740     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqSingletonConcrete 
419489     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqSingletonConcrete 
419491     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 725.79ns 
419492     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqConcat.proof 
419492     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 57.4ns 
419493     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
421756     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.26s 
421756     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqConcat 
422485     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqConcat 
422493     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 6.07ms 
422494     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqSub.proof 
422494     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 64.5ns 
422495     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
424783     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.29s 
424783     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqSub 
425531     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqSub 
425533     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.14ms 
425534     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqReverse.proof 
425534     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 59ns 
425535     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
427788     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.25s 
427788     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqReverse 
428537     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqReverse 
428542     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.25ms 
428543     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqEmpty.proof 
428544     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 56.6ns 
428544     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
430816     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.27s 
430816     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqEmpty 
431547     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqEmpty 
431549     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 689.09ns 
431551     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqSingleton.proof 
431551     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 55ns 
431551     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
433817     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.27s 
433817     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqSingleton 
434566     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqSingleton 
434568     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 561.99ns 
434570     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqConcat.proof 
434571     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 67.5ns 
434571     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
436819     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.25s 
436819     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqConcat 
437570     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqConcat 
437573     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.26ms 
437575     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqSub.proof 
437575     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 176.2ns 
437576     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
439837     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.26s 
439837     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqSub 
440584     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqSub 
440586     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 697.69ns 
440587     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqReverse.proof 
440587     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 59ns 
440588     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
442834     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.25s 
442834     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqReverse 
443581     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqReverse 
443584     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 923.19ns 
443585     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_equalityToSeqGetAndSeqLenLeft.proof 
443585     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 55ns 
443586     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
445851     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.26s 
445851     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: equalityToSeqGetAndSeqLenLeft 
446579     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: equalityToSeqGetAndSeqLenLeft 
446582     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 915.99ns 
446583     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_equalityToSeqGetAndSeqLenRight.proof 
446583     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 60.6ns 
446583     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
448852     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.27s 
448852     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: equalityToSeqGetAndSeqLenRight 
449601     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: equalityToSeqGetAndSeqLenRight 
449605     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.04ms 
449606     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqSingletonEQ.proof 
449606     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 52.9ns 
449607     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
451869     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.26s 
451869     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqSingletonEQ 
452597     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqSingletonEQ 
452599     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 817.89ns 
452600     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqConcatEQ.proof 
452600     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 59.8ns 
452601     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
454868     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.27s 
454868     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqConcatEQ 
455613     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqConcatEQ 
455622     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 6.41ms 
455623     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqSubEQ.proof 
455623     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 59.6ns 
455623     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
457887     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.26s 
457887     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqSubEQ 
458617     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqSubEQ 
458618     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 440.19ns 
458619     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqReverseEQ.proof 
458620     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 56.2ns 
458620     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
460883     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.26s 
460883     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqReverseEQ 
461631     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqReverseEQ 
461637     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.44ms 
461638     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqEmptyEQ.proof 
461638     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 47.5ns 
461639     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
463886     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.25s 
463887     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqEmptyEQ 
464633     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqEmptyEQ 
464635     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 733.39ns 
464636     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqSingletonEQ.proof 
464636     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 45.4ns 
464637     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
466922     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.29s 
466922     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqSingletonEQ 
467670     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqSingletonEQ 
467672     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 687.69ns 
467673     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqConcatEQ.proof 
467673     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 57.6ns 
467674     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
469940     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.27s 
469940     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqConcatEQ 
470671     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqConcatEQ 
470674     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.76ms 
470675     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqSubEQ.proof 
470675     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 63.5ns 
470676     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
472942     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.27s 
472942     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqSubEQ 
473690     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqSubEQ 
473693     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 841.99ns 
473695     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqReverseEQ.proof 
473695     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 170.2ns 
473696     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
475966     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.27s 
475966     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqReverseEQ 
476695     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqReverseEQ 
476698     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.14ms 
476699     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqDefEQ.proof 
476699     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 55.7ns 
476700     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
478961     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.26s 
478961     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqDefEQ 
479711     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqDefEQ 
479714     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.09ms 
479715     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqDefEQ.proof 
479715     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 49.8ns 
479716     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
481988     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.27s 
481988     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqDefEQ 
482741     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqDefEQ 
482745     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.08ms 
482746     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqConcatWithSeqEmpty1.proof 
482746     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 45ns 
482747     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
485002     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.25s 
485002     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqConcatWithSeqEmpty1 
485754     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqConcatWithSeqEmpty1 
485761     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 5.21ms 
485763     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqConcatWithSeqEmpty2.proof 
485763     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 192.2ns 
485764     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
488053     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.29s 
488053     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqConcatWithSeqEmpty2 
488806     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqConcatWithSeqEmpty2 
488813     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 5.41ms 
488814     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqReverseOfSeqEmpty.proof 
488814     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 61ns 
488815     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
491068     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.25s 
491068     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqReverseOfSeqEmpty 
491816     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqReverseOfSeqEmpty 
491821     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.89ms 
491822     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_subSeqComplete.proof 
491822     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 49.1ns 
491823     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
494087     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.26s 
494088     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: subSeqComplete 
494836     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: subSeqComplete 
494842     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.97ms 
494843     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_subSeqTailR.proof 
494843     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 49.4ns 
494843     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
497145     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.3s 
497146     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: subSeqTailR 
497896     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: subSeqTailR 
497905     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 7.53ms 
497907     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_subSeqTailL.proof 
497907     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 57.5ns 
497907     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
500163     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.26s 
500164     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: subSeqTailL 
500913     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: subSeqTailL 
500923     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 7.65ms 
500924     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_subSeqTailEQR.proof 
500924     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 92.6ns 
500925     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
503193     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.27s 
503193     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: subSeqTailEQR 
503940     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: subSeqTailEQR 
503950     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 6.86ms 
503951     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_subSeqTailEQL.proof 
503951     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 61.7ns 
503951     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
506217     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.27s 
506217     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: subSeqTailEQL 
506947     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: subSeqTailEQL 
506954     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.65ms 
506955     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDef_split.proof 
506955     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 64.1ns 
506956     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
509227     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.27s 
509227     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_split 
509976     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDef_split 
509995     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 15.95ms 
509996     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDef_induction_upper.proof 
509996     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 53.2ns 
509997     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
512264     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.27s 
512264     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_induction_upper 
513015     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDef_induction_upper 
513037     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 18.42ms 
513039     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDef_induction_upper_concrete.proof 
513040     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 179ns 
513040     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
515312     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.27s 
515312     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_induction_upper_concrete 
516061     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDef_induction_upper_concrete 
516080     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 16.07ms 
516081     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDef_induction_lower.proof 
516081     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 63.9ns 
516082     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
518330     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.25s 
518331     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_induction_lower 
519082     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDef_induction_lower 
519100     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 14.87ms 
519101     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDef_induction_lower_concrete.proof 
519101     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 66.6ns 
519102     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
521367     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.26s 
521367     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_induction_lower_concrete 
522117     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDef_induction_lower_concrete 
522135     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 15.18ms 
522137     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDef_split_in_three.proof 
522137     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 69.9ns 
522138     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
524408     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.27s 
524408     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_split_in_three 
525158     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDef_split_in_three 
525203     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 38.56ms 
525205     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDef_empty.proof 
525205     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 61.7ns 
525205     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
527472     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.27s 
527472     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_empty 
528229     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDef_empty 
528233     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.57ms 
528234     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDef_one_summand.proof 
528234     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 46.3ns 
528235     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
530496     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.26s 
530497     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_one_summand 
531246     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDef_one_summand 
531251     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.77ms 
531252     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDef_lower_equals_upper.proof 
531252     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 56.8ns 
531252     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
533511     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.26s 
533511     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_lower_equals_upper 
534259     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDef_lower_equals_upper 
534262     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.7ms 
534263     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDefOfSeq.proof 
534263     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 48.5ns 
534264     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
536531     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.27s 
536531     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDefOfSeq 
537279     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDefOfSeq 
537291     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 8.95ms 
537292     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqSelfDefinitionEQ2.proof 
537292     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 55.2ns 
537293     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
539555     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.26s 
539555     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqSelfDefinitionEQ2 
540303     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqSelfDefinitionEQ2 
540308     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.79ms 
540310     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_indexOfSeqSingleton.proof 
540310     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 49ns 
540310     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
542574     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.26s 
542574     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: indexOfSeqSingleton 
543304     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: indexOfSeqSingleton 
543307     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.16ms 
543308     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_indexOfSeqConcatFirst.proof 
543308     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 59.2ns 
543309     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
545574     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.27s 
545574     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: indexOfSeqConcatFirst 
546326     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: indexOfSeqConcatFirst 
546335     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 7.1ms 
546336     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_indexOfSeqConcatSecond.proof 
546336     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 60.7ns 
546337     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
548606     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.27s 
548606     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: indexOfSeqConcatSecond 
549359     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: indexOfSeqConcatSecond 
549369     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 7.48ms 
549370     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_indexOfSeqSub.proof 
549370     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 64ns 
549371     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
551640     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.27s 
551641     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: indexOfSeqSub 
552390     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: indexOfSeqSub 
552402     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 9.61ms 
552403     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfArray2seq.proof 
552403     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 60ns 
552404     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
554674     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.27s 
554674     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfArray2seq 
555436     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfArray2seq 
555439     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 885.39ns 
555440     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getAnyOfArray2seq.proof 
555440     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 58.6ns 
555441     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
557785     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.34s 
557785     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getAnyOfArray2seq 
558554     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getAnyOfArray2seq 
558557     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.6ms 
558558     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfArray2seq.proof 
558558     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 59ns 
558559     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
560840     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.28s 
560840     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfArray2seq 
561591     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfArray2seq 
561597     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.69ms 
561598     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_getAnyOfNPermInv.proof 
561598     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 63ns 
561598     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
563867     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.27s 
563868     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getAnyOfNPermInv 
564597     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getAnyOfNPermInv 
564601     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.47ms 
564602     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqNPermRange.proof 
564602     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 47.3ns 
564603     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
566868     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.26s 
566868     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqNPermRange 
567617     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqNPermRange 
567657     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 33.92ms 
567658     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermTrans.proof 
567659     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 65.4ns 
567659     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
569945     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.29s 
569945     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermTrans 
570694     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermTrans 
570711     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 13.64ms 
570712     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermRefl.proof 
570712     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 77ns 
570713     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
572991     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.28s 
572991     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermRefl 
573740     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermRefl 
573751     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 8.13ms 
573752     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermSplit.proof 
573752     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 61.6ns 
573752     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
576013     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.26s 
576013     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermSplit 
576763     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermSplit 
576765     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 213.2ns 
576766     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqNPermRight.proof 
576766     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 47.4ns 
576767     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
579054     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.29s 
579054     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqNPermRight 
579807     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqNPermRight 
579880     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 62.71ms 
579882     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermFromSwap.proof 
579882     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 65.2ns 
579883     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
582162     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.28s 
582162     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermFromSwap 
582914     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermFromSwap 
582945     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 26.68ms 
582946     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermTransAlt0.proof 
582946     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 52.4ns 
582947     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
585216     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.27s 
585216     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermTransAlt0 
585966     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermTransAlt0 
585968     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 174.2ns 
585970     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermTransAlt1.proof 
585970     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 59.5ns 
585970     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
588240     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.27s 
588240     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermTransAlt1 
588997     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermTransAlt1 
588999     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 200.2ns 
589000     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermTransAlt2.proof 
589000     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 58.6ns 
589001     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
591280     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.28s 
591280     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermTransAlt2 
592033     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermTransAlt2 
592035     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 189.8ns 
592036     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermTransAlt3.proof 
592036     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 49.7ns 
592037     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
594322     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.29s 
594322     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermTransAlt3 
595074     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermTransAlt3 
595076     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 303.2ns 
595077     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermForall.proof 
595077     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 57.1ns 
595077     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
597341     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.26s 
597341     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermForall 
598090     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermForall 
598167     INFO  Test worker     d.u.i.k.s.SMTFocusResults Analyzing unsat core: (L_1 L_3 L_4) 
598174     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 82.09ms 
598176     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermExists.proof 
598176     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 69.5ns 
598179     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
600474     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.29s 
600474     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermExists 
601227     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermExists 
601268     INFO  Test worker     d.u.i.k.s.SMTFocusResults Analyzing unsat core: (L_1 L_3 L_5 L_6 L_7) 
601269     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 40.43ms 
601270     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm2/Taclet_schiffl_lemma_2.proof 
601270     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 56.8ns 
601271     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
603542     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.27s 
603542     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: schiffl_lemma_2 
604296     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: schiffl_lemma_2 
604298     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.2ns 
604325     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [1] goal: 0, source line: 49, command: 'macro split-prop' 
604376     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [2] goal: 3, source line: 50, command: 'rule allRight' 
604395     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [3] goal: 4, source line: 51, command: 'rule allRight' 
604401     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [4] goal: 5, source line: 52, command: 'macro split-prop' 
604416     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [5] goal: 11, source line: 53, command: 'rule 'seqPermDefLeft'' 
604418     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [6] goal: 12, source line: 54, command: 'rule 'andLeft'' 
604420     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [7] goal: 13, source line: 55, command: 'rule 'exLeft'' 
604421     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [8] goal: 14, source line: 56, command: 'macro split-prop' 
604427     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [9] goal: 16, source line: 57, command: 'rule  seqNPermRange' 
604429     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' 
604432     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [11] goal: 18, source line: 60, command: 'rule impLeft' 
604434     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [12] goal: 19, source line: 61, command: 'tryclose branch' 
604677     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [13] goal: 20, source line: 62, command: 'rule andLeft' 
604678     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [14] goal: 97, source line: 63, command: 'rule andLeft' 
604680     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' 
604681     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [16] goal: 99, source line: 66, command: 'rule impLeft' 
604683     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [17] goal: 100, source line: 67, command: 'tryclose branch' 
604832     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [18] goal: 101, source line: 68, command: 'rule andLeft' 
604833     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [19] goal: 188, source line: 69, command: 'rule andLeft' 
604836     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [20] goal: 189, source line: 70, command: 'rule seqNPermDefLeft' 
604837     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' 
604839     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [22] goal: 191, source line: 73, command: 'rule impLeft' 
604841     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [23] goal: 192, source line: 74, command: 'tryclose branch' 
605019     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [24] goal: 193, source line: 75, command: 'rule exLeft' 
605021     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [25] goal: 310, source line: 76, command: 'rule andLeft' 
605022     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [26] goal: 311, source line: 77, command: 'rule andLeft' 
605023     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' 
605023     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [28] goal: 313, source line: 80, command: 'rule impLeft' 
605026     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [29] goal: 314, source line: 81, command: 'tryclose branch' 
605158     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [30] goal: 315, source line: 82, command: 'rule exLeft' 
605159     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [31] goal: 420, source line: 83, command: 'rule andLeft' 
605160     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [32] goal: 421, source line: 84, command: 'rule andLeft' 
605161     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' 
605162     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [34] goal: 423, source line: 87, command: 'rule impLeft' 
605163     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [35] goal: 424, source line: 88, command: 'tryclose branch' 
605171     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [36] goal: 425, source line: 89, command: 'rule andLeft' 
605172     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [37] goal: 434, source line: 90, command: 'rule andLeft' 
605174     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' 
605174     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' 
605176     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [40] goal: 437, source line: 94, command: 'rule impLeft' 
605177     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [41] goal: 438, source line: 95, command: 'tryclose branch' 
605187     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [42] goal: 439, source line: 96, command: 'rule andLeft' 
605187     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [43] goal: 448, source line: 97, command: 'rule andLeft' 
605188     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' 
605189     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [45] goal: 450, source line: 99, command: 'instantiate var=iv  with='v_x_0'' 
605191     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [46] goal: 451, source line: 101, command: 'rule impLeft' 
605191     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [47] goal: 452, source line: 102, command: 'tryclose branch' 
605325     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [48] goal: 453, source line: 103, command: 'instantiate var=iv  with='v_y_0'' 
605326     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [49] goal: 562, source line: 105, command: 'rule impLeft' 
605327     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [50] goal: 563, source line: 106, command: 'tryclose branch' 
605454     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [51] goal: 564, source line: 107, command: 'cut 'v_x_0 = v_y_0'' 
605455     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)'' 
605457     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [53] goal: 676, source line: 111, command: 'rule andRight' 
605459     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [54] goal: 677, source line: 113, command: 'rule andRight' 
605460     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [55] goal: 679, source line: 114, command: 'rule andRight' 
605460     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [56] goal: 681, source line: 115, command: 'rule andRight' 
605463     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [57] goal: 683, source line: 116, command: 'rule lenOfSwap' 
605464     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [58] goal: 685, source line: 117, command: 'tryclose branch' 
605468     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [59] goal: 684, source line: 118, command: 'rule seqNPermSwapNPerm' 
605468     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' 
605470     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [61] goal: 688, source line: 121, command: 'instantiate hide var='jv' with='jv_0'' 
605471     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [62] goal: 689, source line: 122, command: 'rule impLeft' 
605472     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [63] goal: 690, source line: 123, command: 'tryclose branch' 
605580     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [64] goal: 691, source line: 124, command: 'tryclose branch' 
605584     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [65] goal: 682, source line: 125, command: 'rule allRight' 
605585     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [66] goal: 796, source line: 127, command: 'rule impRight' 
605586     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [67] goal: 797, source line: 128, command: 'rule andLeft' 
605588     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [68] goal: 798, source line: 129, command: 'instantiate var=iv with='v_iv_0'' 
605588     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [69] goal: 799, source line: 130, command: 'rule impLeft' 
605593     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [70] goal: 800, source line: 131, command: 'tryclose branch' 
605718     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [71] goal: 801, source line: 132, command: 'rule getOfSwap' 
605719     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [72] goal: 912, source line: 133, command: 'rule ifthenelse_negated' 
605721     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [73] goal: 913, source line: 134, command: 'rule ifthenelse_split occ=0' 
605723     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [74] goal: 914, source line: 135, command: 'rule andLeft' 
605724     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [75] goal: 916, source line: 136, command: 'rule andLeft' 
605724     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [76] goal: 917, source line: 137, command: 'rule andLeft' 
605726     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [77] goal: 918, source line: 138, command: 'rule ifthenelse_split occ=0' 
605727     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [78] goal: 919, source line: 139, command: 'tryclose branch' 
605833     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [79] goal: 920, source line: 140, command: 'rule ifthenelse_split occ=0' 
605834     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [80] goal: 1011, source line: 141, command: 'tryclose branch' 
605929     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [81] goal: 1012, source line: 142, command: 'tryclose branch' 
605934     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [82] goal: 915, source line: 143, command: 'tryclose branch' 
605940     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [83] goal: 680, source line: 144, command: 'rule getOfSwap' 
605940     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [84] goal: 1099, source line: 146, command: 'rule ifthenelse_negated' 
605944     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [85] goal: 1100, source line: 147, command: 'rule ifthenelse_split occ=0' 
605945     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [86] goal: 1101, source line: 148, command: 'rule andLeft' 
605946     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [87] goal: 1103, source line: 149, command: 'rule andLeft' 
605946     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [88] goal: 1104, source line: 150, command: 'rule andLeft' 
605947     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [89] goal: 1105, source line: 151, command: 'rule ifthenelse_split occ=0' 
605947     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [90] goal: 1106, source line: 152, command: 'tryclose branch' 
605956     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [91] goal: 1107, source line: 153, command: 'tryclose branch' 
605961     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [92] goal: 1102, source line: 154, command: 'tryclose branch' 
606062     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [93] goal: 678, source line: 155, command: 'rule getOfSwap' 
606064     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [94] goal: 1225, source line: 157, command: 'rule ifthenelse_negated' 
606066     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [95] goal: 1226, source line: 158, command: 'rule ifthenelse_split occ=0' 
606067     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [96] goal: 1227, source line: 159, command: 'rule andLeft' 
606068     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [97] goal: 1229, source line: 160, command: 'rule andLeft' 
606068     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [98] goal: 1230, source line: 161, command: 'rule andLeft' 
606069     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [99] goal: 1231, source line: 162, command: 'rule ifthenelse_split occ=0' 
606069     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [100] goal: 1232, source line: 163, command: 'tryclose branch' 
606124     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [101] goal: 1233, source line: 164, command: 'tryclose branch' 
606130     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [102] goal: 1228, source line: 165, command: 'tryclose branch' 
606235     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]'' 
606236     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [104] goal: 1397, source line: 169, command: 'rule seqNPermInjective' 
606238     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'' 
606239     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'' 
606240     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [107] goal: 1401, source line: 172, command: 'rule impLeft' 
606242     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [108] goal: 1402, source line: 173, command: 'tryclose branch' 
606407     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [109] goal: 1403, source line: 174, command: 'tryclose branch' 
606412     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'' 
606413     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)'' 
606414     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [112] goal: 1536, source line: 179, command: 'rule andRight' 
606415     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [113] goal: 1537, source line: 181, command: 'rule andRight' 
606425     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [114] goal: 1539, source line: 182, command: 'rule andRight' 
606428     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [115] goal: 1541, source line: 183, command: 'rule andRight' 
606428     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [116] goal: 1543, source line: 184, command: 'tryclose branch' 
606440     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [117] goal: 1544, source line: 185, command: 'rule seqNPermSwapNPerm' 
606441     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'' 
606442     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [119] goal: 1559, source line: 188, command: 'instantiate hide var=jv with='jv_1'' 
606443     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [120] goal: 1560, source line: 189, command: 'tryclose branch' 
606543     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [121] goal: 1542, source line: 190, command: 'rule allRight' 
606544     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [122] goal: 1667, source line: 192, command: 'rule impRight' 
606545     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [123] goal: 1668, source line: 193, command: 'rule andLeft' 
606546     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [124] goal: 1669, source line: 194, command: 'instantiate var=iv with='v_iv_0'' 
606547     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [125] goal: 1670, source line: 195, command: 'rule impLeft' 
606547     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [126] goal: 1671, source line: 196, command: 'tryclose branch' 
606684     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [127] goal: 1672, source line: 197, command: 'rule getOfSwap' 
606685     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [128] goal: 1786, source line: 198, command: 'rule ifthenelse_negated' 
606686     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [129] goal: 1787, source line: 199, command: 'rule ifthenelse_split occ=0' 
606687     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [130] goal: 1788, source line: 200, command: 'rule andLeft' 
606688     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [131] goal: 1790, source line: 201, command: 'rule andLeft' 
606689     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [132] goal: 1791, source line: 202, command: 'rule andLeft' 
606689     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [133] goal: 1792, source line: 203, command: 'rule ifthenelse_split occ=0' 
606690     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [134] goal: 1793, source line: 204, command: 'tryclose branch' 
606767     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [135] goal: 1794, source line: 205, command: 'rule ifthenelse_split occ=0' 
606768     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [136] goal: 1885, source line: 206, command: 'tryclose branch' 
606837     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [137] goal: 1886, source line: 207, command: 'instantiate var=iv with='v_y_0'' 
606837     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [138] goal: 1968, source line: 208, command: 'rule impLeft' 
606839     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [139] goal: 1969, source line: 209, command: 'tryclose branch' 
606843     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [140] goal: 1970, source line: 210, command: 'tryclose branch' 
606846     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [141] goal: 1789, source line: 211, command: 'tryclose branch' 
606850     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [142] goal: 1540, source line: 212, command: 'tryclose branch' 
606958     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [143] goal: 1538, source line: 213, command: 'rule getOfSwap' 
606959     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [144] goal: 2097, source line: 215, command: 'rule ifthenelse_negated' 
606965     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [145] goal: 2098, source line: 216, command: 'rule ifthenelse_split occ=0' 
606966     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [146] goal: 2099, source line: 217, command: 'tryclose branch' 
606975     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [147] goal: 2100, source line: 218, command: 'tryclose branch' 
607051     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [148] goal: 1535, source line: 219, command: 'tryclose branch' 
610294     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'' 
610294     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)'' 
610298     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [151] goal: 4268, source line: 226, command: 'rule andRight' 
610300     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [152] goal: 4269, source line: 228, command: 'rule andRight' 
610301     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [153] goal: 4271, source line: 229, command: 'rule andRight' 
610301     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [154] goal: 4273, source line: 230, command: 'rule andRight' 
610302     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [155] goal: 4275, source line: 231, command: 'tryclose branch' 
610309     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [156] goal: 4276, source line: 232, command: 'rule seqNPermSwapNPerm' 
610310     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'' 
610311     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [158] goal: 4288, source line: 235, command: 'instantiate hide var=jv with='jv_0'' 
610312     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [159] goal: 4289, source line: 236, command: 'rule impLeft' 
610312     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [160] goal: 4290, source line: 237, command: 'tryclose branch' 
610401     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [161] goal: 4291, source line: 238, command: 'tryclose branch' 
610404     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [162] goal: 4274, source line: 239, command: 'rule allRight' 
610405     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [163] goal: 4400, source line: 241, command: 'rule impRight' 
610406     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [164] goal: 4401, source line: 242, command: 'rule andLeft' 
610407     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [165] goal: 4402, source line: 243, command: 'instantiate var=iv with='v_iv_0'' 
610407     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [166] goal: 4403, source line: 244, command: 'rule impLeft' 
610409     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [167] goal: 4404, source line: 245, command: 'tryclose branch' 
610554     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [168] goal: 4405, source line: 246, command: 'rule getOfSwap' 
610555     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [169] goal: 4521, source line: 247, command: 'rule ifthenelse_negated' 
610556     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [170] goal: 4522, source line: 248, command: 'rule ifthenelse_split occ=0' 
610558     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [171] goal: 4523, source line: 249, command: 'rule andLeft' 
610559     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [172] goal: 4525, source line: 250, command: 'rule andLeft' 
610559     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [173] goal: 4526, source line: 251, command: 'rule andLeft' 
610560     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [174] goal: 4527, source line: 252, command: 'rule ifthenelse_split occ=0' 
610560     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [175] goal: 4528, source line: 253, command: 'tryclose branch' 
610632     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [176] goal: 4529, source line: 254, command: 'rule ifthenelse_split occ=0' 
610633     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [177] goal: 4622, source line: 255, command: 'tryclose branch' 
610703     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [178] goal: 4623, source line: 256, command: 'tryclose branch' 
610707     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [179] goal: 4524, source line: 257, command: 'tryclose branch' 
610711     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [180] goal: 4272, source line: 258, command: 'rule getOfSwap' 
610711     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [181] goal: 4713, source line: 260, command: 'rule ifthenelse_negated' 
610712     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [182] goal: 4714, source line: 261, command: 'rule ifthenelse_split occ=0' 
610712     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [183] goal: 4715, source line: 262, command: 'tryclose branch' 
610722     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [184] goal: 4716, source line: 263, command: 'tryclose branch' 
610800     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [185] goal: 4270, source line: 264, command: 'rule getOfSwap' 
610801     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [186] goal: 4839, source line: 266, command: 'rule ifthenelse_negated' 
610802     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [187] goal: 4840, source line: 267, command: 'rule ifthenelse_split occ=0' 
610802     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [188] goal: 4841, source line: 268, command: 'tryclose branch' 
610870     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [189] goal: 4842, source line: 269, command: 'tryclose branch' 
610880     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'' 
610881     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)'' 
610882     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [192] goal: 4950, source line: 275, command: 'rule andRight' 
610884     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [193] goal: 4951, source line: 277, command: 'rule andRight' 
610884     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [194] goal: 4953, source line: 278, command: 'rule andRight' 
610885     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [195] goal: 4955, source line: 279, command: 'rule andRight' 
610885     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [196] goal: 4957, source line: 280, command: 'tryclose branch' 
610896     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [197] goal: 4958, source line: 281, command: 'rule seqNPermSwapNPerm' 
610896     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [198] goal: 4977, source line: 283, command: 'instantiate hide var=iv with='jv_0'' 
610897     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'' 
610899     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [200] goal: 4979, source line: 285, command: 'rule impLeft' 
610900     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [201] goal: 4980, source line: 286, command: 'tryclose branch' 
610981     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))'' 
610982     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [203] goal: 5093, source line: 288, command: 'instantiate hide var=iv with='jv_0'' 
610984     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'' 
610985     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [205] goal: 5095, source line: 290, command: 'rule impLeft' 
610988     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [206] goal: 5096, source line: 291, command: 'tryclose branch' 
611076     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [207] goal: 5097, source line: 292, command: 'tryclose branch' 
611080     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [208] goal: 4956, source line: 293, command: 'rule allRight' 
611081     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [209] goal: 5212, source line: 295, command: 'rule impRight' 
611082     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [210] goal: 5213, source line: 296, command: 'rule andLeft' 
611082     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [211] goal: 5214, source line: 297, command: 'instantiate var=iv with='v_iv_0'' 
611083     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [212] goal: 5215, source line: 300, command: 'rule impLeft' 
611084     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [213] goal: 5216, source line: 301, command: 'tryclose branch' 
611174     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [214] goal: 5217, source line: 302, command: 'rule getOfSwap' 
611175     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [215] goal: 5337, source line: 304, command: 'rule ifthenelse_negated' 
611177     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [216] goal: 5338, source line: 305, command: 'rule ifthenelse_split occ=0' 
611177     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [217] goal: 5339, source line: 306, command: 'rule andLeft' 
611178     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [218] goal: 5341, source line: 307, command: 'rule andLeft' 
611180     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [219] goal: 5342, source line: 308, command: 'rule andLeft' 
611181     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [220] goal: 5343, source line: 309, command: 'rule ifthenelse_split occ=0' 
611182     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [221] goal: 5344, source line: 310, command: 'rule getOfSwap' 
611182     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [222] goal: 5346, source line: 311, command: 'rule ifthenelse_negated' 
611183     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [223] goal: 5347, source line: 312, command: 'rule ifthenelse_split occ=0' 
611184     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [224] goal: 5348, source line: 313, command: 'rule andLeft' 
611185     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [225] goal: 5350, source line: 314, command: 'rule andLeft' 
611185     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [226] goal: 5351, source line: 315, command: 'rule andLeft' 
611186     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [227] goal: 5352, source line: 316, command: 'rule ifthenelse_split occ=0' 
611186     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [228] goal: 5353, source line: 317, command: 'tryclose branch' 
611269     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [229] goal: 5354, source line: 318, command: 'rule ifthenelse_split occ=0' 
611270     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [230] goal: 5463, source line: 319, command: 'tryclose branch' 
611276     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [231] goal: 5464, source line: 320, command: 'tryclose branch' 
611347     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [232] goal: 5349, source line: 321, command: 'tryclose branch' 
611421     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [233] goal: 5345, source line: 322, command: 'rule ifthenelse_split' 
611422     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [234] goal: 5660, source line: 324, command: 'rule getOfSwap' 
611423     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [235] goal: 5662, source line: 325, command: 'rule ifthenelse_negated' 
611423     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [236] goal: 5663, source line: 326, command: 'rule ifthenelse_split occ=0' 
611424     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [237] goal: 5664, source line: 327, command: 'rule andLeft' 
611425     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [238] goal: 5666, source line: 328, command: 'rule andLeft' 
611425     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [239] goal: 5667, source line: 329, command: 'rule andLeft' 
611425     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [240] goal: 5668, source line: 330, command: 'rule ifthenelse_split occ=0' 
611426     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [241] goal: 5669, source line: 331, command: 'tryclose branch' 
611504     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [242] goal: 5670, source line: 332, command: 'tryclose branch' 
611510     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [243] goal: 5665, source line: 333, command: 'tryclose branch' 
611591     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [244] goal: 5661, source line: 334, command: 'rule getOfSwap' 
611592     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [245] goal: 5887, source line: 336, command: 'rule ifthenelse_negated' 
611593     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [246] goal: 5888, source line: 337, command: 'rule ifthenelse_split occ=0' 
611593     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [247] goal: 5889, source line: 338, command: 'rule andLeft' 
611594     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [248] goal: 5891, source line: 339, command: 'rule andLeft' 
611594     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [249] goal: 5892, source line: 340, command: 'rule andLeft' 
611594     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [250] goal: 5893, source line: 341, command: 'rule ifthenelse_split occ=0' 
611595     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [251] goal: 5894, source line: 342, command: 'tryclose branch' 
611600     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [252] goal: 5895, source line: 343, command: 'rule ifthenelse_split occ=0' 
611600     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [253] goal: 5897, source line: 344, command: 'tryclose branch' 
611673     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [254] goal: 5898, source line: 345, command: 'tryclose branch' 
611678     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [255] goal: 5890, source line: 346, command: 'tryclose branch' 
611683     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [256] goal: 5340, source line: 347, command: 'tryclose branch' 
611774     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [257] goal: 4954, source line: 348, command: 'rule getOfSwap' 
611775     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [258] goal: 6115, source line: 350, command: 'rule ifthenelse_negated' 
611775     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [259] goal: 6116, source line: 351, command: 'rule ifthenelse_split occ=0' 
611776     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [260] goal: 6117, source line: 352, command: 'rule andLeft' 
611776     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [261] goal: 6119, source line: 353, command: 'rule andLeft' 
611777     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [262] goal: 6120, source line: 354, command: 'rule andLeft' 
611777     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [263] goal: 6121, source line: 355, command: 'rule ifthenelse_split occ=0' 
611777     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [264] goal: 6122, source line: 356, command: 'tryclose branch' 
611827     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [265] goal: 6123, source line: 357, command: 'rule ifthenelse_split occ=0' 
611828     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [266] goal: 6193, source line: 358, command: 'rule getOfSwap' 
611829     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [267] goal: 6195, source line: 359, command: 'rule ifthenelse_negated' 
611829     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [268] goal: 6196, source line: 360, command: 'rule ifthenelse_split occ=0' 
611830     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [269] goal: 6197, source line: 361, command: 'tryclose branch' 
611835     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [270] goal: 6198, source line: 362, command: 'tryclose branch' 
611839     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [271] goal: 6194, source line: 363, command: 'tryclose branch' 
611946     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [272] goal: 6118, source line: 364, command: 'tryclose branch' 
612027     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [273] goal: 4952, source line: 365, command: 'rule getOfSwap' 
612027     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [274] goal: 6456, source line: 367, command: 'rule ifthenelse_negated' 
612028     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [275] goal: 6457, source line: 368, command: 'rule ifthenelse_split occ=0' 
612029     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [276] goal: 6458, source line: 369, command: 'tryclose branch' 
612223     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [277] goal: 6459, source line: 370, command: 'tryclose branch' 
612304     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'' 
612304     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [279] goal: 6735, source line: 375, command: 'tryclose branch' 
615044     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [280] goal: 6735, source line: 378, command: 'rule seqNPermSwapNPerm' 
615048     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [281] goal: 8783, source line: 380, command: 'instantiate hide var=iv with='jv_1'' 
615049     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'' 
615050     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [283] goal: 8785, source line: 382, command: 'rule impLeft' 
615050     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [284] goal: 8786, source line: 383, command: 'tryclose branch' 
615156     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))'' 
615157     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [286] goal: 8909, source line: 385, command: 'instantiate hide var=iv with='jv_1'' 
615157     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'' 
615158     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [288] goal: 8911, source line: 387, command: 'rule impLeft' 
615159     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [289] goal: 8912, source line: 388, command: 'tryclose branch' 
615256     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [290] goal: 8913, source line: 389, command: 'tryclose branch' 
617996     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [291] goal: 6736, source line: 390, command: 'tryclose branch' 
620943     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [292] goal: 6736, source line: 397, command: 'rule seqNPermSwapNPerm formula='seqNPerm(s_0)'' 
620946     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'' 
620947     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [294] goal: 12634, source line: 400, command: 'instantiate hide var=jv with='jv_0'' 
620948     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [295] goal: 12635, source line: 401, command: 'rule impLeft' 
620949     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [296] goal: 12636, source line: 402, command: 'tryclose branch' 
621053     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))'' 
621054     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'' 
621055     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [299] goal: 12758, source line: 405, command: 'instantiate hide var=jv with='jv_1'' 
621056     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)' ...' 
621056     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [301] goal: 12760, source line: 407, command: 'tryclose branch' 
622118     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm2/Taclet_schiffl_thm_1.proof 
622118     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 82.7ns 
622119     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
624450     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.33s 
624450     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: schiffl_thm_1 
625221     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: schiffl_thm_1 
625223     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 8ns 
625223     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [1] goal: 0, source line: 50, command: 'macro split-prop' 
625232     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)'' 
625240     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [3] goal: 11, source line: 52, command: 'instantiate hide var=x with='f_x'' 
625242     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [4] goal: 12, source line: 53, command: 'instantiate hide var=y with='f_y'' 
625244     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [5] goal: 13, source line: 54, command: 'rule impLeft' 
625246     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [6] goal: 14, source line: 55, command: 'tryclose branch' 
625250     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [7] goal: 15, source line: 56, command: 'rule exLeft' 
625251     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [8] goal: 23, source line: 57, command: 'macro split-prop' 
625255     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [9] goal: 27, source line: 58, command: 'rule seqPermDef occ=1' 
625255     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [10] goal: 28, source line: 59, command: 'rule andRight' 
625257     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [11] goal: 29, source line: 60, command: 'tryclose branch' 
625267     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [12] goal: 30, source line: 61, command: 'instantiate hide var=s with='r_0'' 
625267     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [13] goal: 46, source line: 62, command: 'rule andRight' 
625269     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [14] goal: 47, source line: 63, command: 'tryclose branch' 
625317     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [15] goal: 48, source line: 64, command: 'rule allRight' 
625317     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [16] goal: 119, source line: 65, command: 'rule impRight' 
625318     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [17] goal: 120, source line: 66, command: 'instantiate hide var=iv with='iv_0'' 
625318     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [18] goal: 121, source line: 67, command: 'rule impLeft' 
625319     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [19] goal: 122, source line: 68, command: 'tryclose branch' 
625385     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [20] goal: 123, source line: 69, command: 'rule andLeft' 
625386     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [21] goal: 203, source line: 70, command: 'rule seqNPermRange' 
625386     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [22] goal: 204, source line: 71, command: 'instantiate hide var=iv with='iv_0'' 
625387     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [23] goal: 205, source line: 72, command: 'rule impLeft' 
625388     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [24] goal: 206, source line: 73, command: 'tryclose branch' 
625392     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [25] goal: 207, source line: 74, command: 'rule andLeft' 
625392     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [26] goal: 215, source line: 75, command: 'rule andLeft' 
625392     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [27] goal: 216, source line: 76, command: 'rule seqNPermRange' 
625393     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [28] goal: 217, source line: 77, command: 'instantiate hide var=iv with='f_x'' 
625393     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [29] goal: 218, source line: 78, command: 'rule impLeft' 
625394     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [30] goal: 219, source line: 79, command: 'tryclose branch' 
625476     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [31] goal: 220, source line: 80, command: 'rule andLeft' 
625476     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [32] goal: 311, source line: 81, command: 'rule andLeft' 
625477     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [33] goal: 312, source line: 82, command: 'rule seqNPermRange' 
625477     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [34] goal: 313, source line: 83, command: 'instantiate hide var=iv with='f_y'' 
625478     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [35] goal: 314, source line: 84, command: 'rule impLeft' 
625479     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [36] goal: 315, source line: 85, command: 'tryclose branch' 
625559     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [37] goal: 316, source line: 86, command: 'rule andLeft' 
625560     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [38] goal: 410, source line: 87, command: 'rule andLeft' 
625561     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [39] goal: 411, source line: 88, command: 'rule getOfSeqDef occ=0' 
625561     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [40] goal: 412, source line: 89, command: 'rule getOfSeqDef' 
625562     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [41] goal: 413, source line: 90, command: 'rule ifthenelse_split occ=0' 
625562     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [42] goal: 414, source line: 91, command: 'rule andLeft occ=0' 
625563     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [43] goal: 416, source line: 92, command: 'rule sub_zero_2 occ=0' 
625563     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [44] goal: 417, source line: 93, command: 'rule ifthenelse_split occ=2' 
625564     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [45] goal: 418, source line: 94, command: 'rule andLeft' 
625565     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [46] goal: 420, source line: 95, command: 'rule sub_zero_2 occ=0' 
625565     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [47] goal: 421, source line: 96, command: 'rule add_zero_right occ=0' 
625565     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [48] goal: 422, source line: 97, command: 'rule add_zero_right occ=0' 
625566     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [49] goal: 423, source line: 98, command: 'rule add_zero_right occ=0' 
625566     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [50] goal: 424, source line: 99, command: 'rule add_zero_right occ=0' 
625567     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [51] goal: 425, source line: 100, command: 'rule add_zero_right occ=0' 
625567     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [52] goal: 426, source line: 101, command: 'rule add_zero_right occ=0' 
625568     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [53] goal: 427, source line: 102, command: 'rule ifthenelse_split occ=0' 
625568     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [54] goal: 428, source line: 103, command: 'rule ifthenelse_split occ=0' 
625569     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [55] goal: 430, source line: 104, command: 'tryclose branch' 
625571     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [56] goal: 431, source line: 105, command: 'tryclose branch' 
625607     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [57] goal: 429, source line: 106, command: 'rule ifthenelse_split occ=0' 
625608     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [58] goal: 473, source line: 107, command: 'tryclose branch' 
625662     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [59] goal: 474, source line: 108, command: 'rule ifthenelse_split occ=0' 
625663     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [60] goal: 541, source line: 109, command: 'rule seqNPermInjective' 
625663     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [61] goal: 543, source line: 110, command: 'instantiate hide var=iv with='iv_0'' 
625665     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [62] goal: 544, source line: 111, command: 'instantiate hide var=jv with='f_y'' 
625666     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [63] goal: 545, source line: 112, command: 'rule impLeft' 
625666     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [64] goal: 546, source line: 113, command: 'tryclose branch' 
625717     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [65] goal: 547, source line: 114, command: 'tryclose branch' 
625720     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [66] goal: 542, source line: 115, command: 'rule ifthenelse_split occ=0' 
625721     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [67] goal: 606, source line: 116, command: 'rule seqNPermInjective' 
625722     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [68] goal: 608, source line: 117, command: 'instantiate hide var=iv with='iv_0'' 
625723     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [69] goal: 609, source line: 118, command: 'instantiate hide var=jv with='f_x'' 
625724     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [70] goal: 610, source line: 119, command: 'rule impLeft' 
625724     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [71] goal: 611, source line: 120, command: 'tryclose branch' 
625830     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [72] goal: 612, source line: 121, command: 'tryclose branch' 
625832     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [73] goal: 607, source line: 122, command: 'tryclose branch' 
625835     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [74] goal: 419, source line: 123, command: 'tryclose branch' 
625892     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [75] goal: 415, source line: 124, command: 'tryclose branch' 
625943     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_eqSameSeq.proof 
625943     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 211.1ns 
625944     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
628270     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.33s 
628270     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: eqSameSeq 
629060     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: eqSameSeq 
629075     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 11.61ms