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

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

tests
0

failures
0

ignored
10m38.81s

duration
100%

successful

Tests

Test Method name Duration Result
powPositive data()[100] 3.100s passed
powPositiveConcrete data()[101] 3.061s passed
powGeq1Concrete data()[102] 3.042s passed
pow2InIntLower data()[103] 3.071s passed
pow2InIntUpper data()[104] 3.059s passed
logSelfConcrete data()[105] 3.097s passed
log1Concrete data()[106] 3.110s passed
logProduct data()[107] 3.086s passed
logTimesBaseConcrete data()[108] 3.046s passed
logProdIdentity data()[109] 3.079s passed
moduloByteIsInByte data()[10] 3.214s passed
logProdIdentityConcrete data()[110] 3.052s passed
logPowIdentity data()[111] 3.083s passed
logPowIdentityConcrete data()[112] 3.060s passed
logPositive data()[113] 3.105s passed
logPositiveConcrete data()[114] 3.087s passed
logMono data()[115] 3.127s passed
logMonoConcrete data()[116] 3.096s passed
powLogLess data()[117] 3.120s passed
powLogMore2 data()[118] 3.127s passed
logLessThanPow data()[119] 3.117s passed
moduloCharIsInChar data()[11] 3.180s passed
logLessThanPowConcrete data()[120] 3.154s passed
logSqueeze data()[121] 3.125s passed
ifthenelse_equals data()[122] 3.090s passed
ifthenelse_equals_1 data()[123] 3.093s passed
ifthenelse_equals_2 data()[124] 3.103s passed
disjointWithSingleton1 data()[125] 3.112s passed
disjointWithSingleton2 data()[126] 3.223s passed
disjointArrayRanges data()[127] 3.125s passed
disjointArrayRangeAllFields1 data()[128] 3.086s passed
disjointArrayRangeAllFields2 data()[129] 3.102s passed
div_unique1 data()[12] 3.277s passed
seqSelfDefinition data()[130] 3.108s passed
seqOutsideValue data()[131] 3.106s passed
castedGetAny data()[132] 3.088s passed
seqGetAlphaCast data()[133] 3.113s passed
getOfSeqSingleton data()[134] 3.109s passed
getOfSeqSingletonConcrete data()[135] 3.108s passed
getOfSeqConcat data()[136] 3.131s passed
getOfSeqSub data()[137] 3.126s passed
getOfSeqReverse data()[138] 3.130s passed
lenOfSeqEmpty data()[139] 3.150s passed
div_unique2 data()[13] 3.207s passed
lenOfSeqSingleton data()[140] 3.136s passed
lenOfSeqConcat data()[141] 3.115s passed
lenOfSeqSub data()[142] 3.122s passed
lenOfSeqReverse data()[143] 3.119s passed
equalityToSeqGetAndSeqLenLeft data()[144] 3.115s passed
equalityToSeqGetAndSeqLenRight data()[145] 3.111s passed
getOfSeqSingletonEQ data()[146] 3.114s passed
getOfSeqConcatEQ data()[147] 3.126s passed
getOfSeqSubEQ data()[148] 3.128s passed
getOfSeqReverseEQ data()[149] 3.111s passed
div_exists data()[14] 3.327s passed
lenOfSeqEmptyEQ data()[150] 3.117s passed
lenOfSeqSingletonEQ data()[151] 3.112s passed
lenOfSeqConcatEQ data()[152] 3.117s passed
lenOfSeqSubEQ data()[153] 3.130s passed
lenOfSeqReverseEQ data()[154] 3.138s passed
getOfSeqDefEQ data()[155] 3.118s passed
lenOfSeqDefEQ data()[156] 3.117s passed
seqConcatWithSeqEmpty1 data()[157] 3.115s passed
seqConcatWithSeqEmpty2 data()[158] 3.123s passed
seqReverseOfSeqEmpty data()[159] 3.142s passed
div_one data()[15] 3.169s passed
subSeqComplete data()[160] 3.109s passed
subSeqTailR data()[161] 3.126s passed
subSeqTailL data()[162] 3.142s passed
subSeqTailEQR data()[163] 3.129s passed
subSeqTailEQL data()[164] 3.122s passed
seqDef_split data()[165] 3.123s passed
seqDef_induction_upper data()[166] 3.165s passed
seqDef_induction_upper_concrete data()[167] 3.128s passed
seqDef_induction_lower data()[168] 3.125s passed
seqDef_induction_lower_concrete data()[169] 3.116s passed
jdiv_one data()[16] 3.157s passed
seqDef_split_in_three data()[170] 3.159s passed
seqDef_empty data()[171] 3.106s passed
seqDef_one_summand data()[172] 3.113s passed
seqDef_lower_equals_upper data()[173] 3.115s passed
seqDefOfSeq data()[174] 3.116s passed
seqSelfDefinitionEQ2 data()[175] 3.121s passed
indexOfSeqSingleton data()[176] 3.092s passed
indexOfSeqConcatFirst data()[177] 3.114s passed
indexOfSeqConcatSecond data()[178] 3.124s passed
indexOfSeqSub data()[179] 3.122s passed
div_zero data()[17] 3.244s passed
lenOfArray2seq data()[180] 3.133s passed
getAnyOfArray2seq data()[181] 3.108s passed
getOfArray2seq data()[182] 3.138s passed
getAnyOfNPermInv data()[183] 3.114s passed
seqNPermRange data()[184] 3.174s passed
seqPermTrans data()[185] 3.137s passed
seqPermRefl data()[186] 3.179s passed
seqPermSplit data()[187] 3.171s passed
seqNPermRight data()[188] 3.248s passed
seqPermFromSwap data()[189] 3.211s passed
divResZero1 data()[18] 3.167s passed
seqPermTransAlt0 data()[190] 3.169s passed
seqPermTransAlt1 data()[191] 3.155s passed
seqPermTransAlt2 data()[192] 3.176s passed
seqPermTransAlt3 data()[193] 3.169s passed
seqPermForall data()[194] 3.322s passed
seqPermExists data()[195] 3.240s passed
schiffl_lemma_2 data()[196] 21.629s passed
schiffl_thm_1 data()[197] 3.874s passed
eqSameSeq data()[198] 3.317s passed
divResZero2 data()[19] 3.183s passed
eqTermCut data()[1] 4.010s passed
divResOne1 data()[20] 3.148s passed
divResOne2 data()[21] 3.290s passed
div_cancel1 data()[22] 3.182s passed
div_cancel2 data()[23] 3.151s passed
divAddMultDenom data()[24] 3.178s passed
divMinus data()[25] 3.197s passed
divMinusDenom data()[26] 3.158s passed
divLeastDPos data()[27] 3.085s passed
divLeastDNeg data()[28] 3.085s passed
divGreatestDPos data()[29] 3.094s passed
equivAllRight data()[2] 3.619s passed
divGreatestDNeg data()[30] 3.105s passed
divIncreasingPos data()[31] 3.109s passed
divIncreasingNeg data()[32] 3.084s passed
jdiv_zero data()[33] 3.082s passed
jdivPulloutMinusNum data()[34] 3.088s passed
jdivPulloutMinusDenom data()[35] 3.112s passed
jdiv_uniquePosPos data()[36] 3.110s passed
jdiv_uniquePosNeg data()[37] 3.093s passed
jdiv_uniqueNegPos data()[38] 3.095s passed
jdiv_uniqueNegNeg data()[39] 3.108s passed
irrflConcrete1 data()[3] 3.444s passed
jdivMultDenom1 data()[40] 3.115s passed
jdivMultDenom2 data()[41] 3.073s passed
mod_geZero data()[42] 3.070s passed
mod_lessDenom data()[43] 3.114s passed
jmod_NumPos data()[44] 3.072s passed
jmod_NumNeg data()[45] 3.067s passed
jmod_geZero data()[46] 3.085s passed
jmodNumZero data()[47] 3.065s passed
jmod_pulloutminusNum data()[48] 3.105s passed
jmod_pulloutminusDenom data()[49] 3.084s passed
irrflConcrete2 data()[4] 3.331s passed
jmodUnique1 data()[50] 3.163s passed
jmodUnique2 data()[51] 3.153s passed
intDivRem data()[52] 3.063s passed
jmodjmod data()[53] 3.126s passed
jmodDivisible data()[54] 3.107s passed
jmodDivisibleRep data()[55] 3.069s passed
jdivAddMultDenom data()[56] 3.163s passed
jmodAltZero data()[57] 3.084s passed
jmodAddMultDenomZero data()[58] 3.062s passed
polyDiv_zero data()[59] 3.071s passed
cancel_gtPos data()[5] 3.386s passed
polyMod_ltdivDenom data()[60] 3.045s passed
bsum_empty data()[61] 3.037s passed
bsum_induction_upper data()[62] 3.075s passed
bsum_induction_lower data()[63] 3.055s passed
bsum_num_of_bounds data()[64] 3.058s passed
bsum_num_of_bounds2 data()[65] 3.032s passed
bsum_induction_upper2 data()[66] 3.023s passed
bsum_induction_upper_concrete data()[67] 3.049s passed
bsum_induction_upper_concrete_2 data()[68] 3.034s passed
bsum_induction_upper2_concrete data()[69] 3.045s passed
cancel_gtNeg data()[6] 3.319s passed
bsum_induction_lower_concrete data()[70] 3.050s passed
bsum_induction_lower2 data()[71] 3.029s passed
bsum_induction_lower2_concrete data()[72] 3.049s passed
bsum_positive data()[73] 3.070s passed
bsum_upper_bound data()[74] 3.089s passed
bsum_lower_bound data()[75] 3.063s passed
bsum_positive_lower_bound_element data()[76] 3.066s passed
bsum_sub_same_index data()[77] 3.047s passed
bsum_less_same_index data()[78] 3.061s passed
bsum_equal_except_one_index data()[79] 3.057s passed
moduloIntIsInInt data()[7] 3.346s passed
bsum_num_of_is_max data()[80] 3.057s passed
bsum_num_of_is_max2 data()[81] 3.123s passed
bsum_num_of_is_max3 data()[82] 3.102s passed
bsum_num_of_is_max4 data()[83] 3.089s passed
bsum_num_of_lt_max data()[84] 3.074s passed
bsum_num_of_lt_max2 data()[85] 3.066s passed
bsum_num_of_lt_max3 data()[86] 3.098s passed
bsum_num_of_lt_max4 data()[87] 3.072s passed
bsum_num_of_gt0 data()[88] 3.095s passed
bsum_num_of_gt0_alt data()[89] 3.059s passed
moduloLongIsInLong data()[8] 3.228s passed
bsum_add_concrete data()[90] 3.055s passed
bprod_all_positive data()[91] 3.078s passed
bprod_split data()[92] 3.056s passed
powConcrete0 data()[93] 3.100s passed
powConcrete1 data()[94] 3.079s passed
powSplitFactor data()[95] 3.092s passed
powAdd data()[96] 3.087s passed
powMono data()[97] 3.099s passed
powMonoConcrete data()[98] 3.081s passed
powMonoConcreteRight data()[99] 3.083s passed
moduloShortIsInShort data()[9] 3.190s passed

Standard output

365        INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src/test/resources/testcase/dummyTrue.key 
389        DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 8.11ms 
629        INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
642        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)

1563       DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for Meta 
1565       DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for Meta 
1566       DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for Meta 
1566       DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for Meta 
2883       DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for JavaBigintExpression 
8303       DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 7.67s 
8366       INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof dummyTrue.key 
8399       DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 48.6ns 
8411       INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/firstOrder/Taclet_eqTermCut.proof 
8411       DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 221.9ns 
8414       INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
11462      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.05s 
11464      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: eqTermCut 
12384      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: eqTermCut 
12412      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 22.04ms 
12426      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/firstOrder/Taclet_equivAllRight.proof 
12426      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 185.4ns 
12430      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
15173      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.74s 
15174      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: equivAllRight 
16029      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: equivAllRight 
16043      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 10.45ms 
16048      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_irrflConcrete1.proof 
16048      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 427.9ns 
16050      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
18643      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.59s 
18645      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: irrflConcrete1 
19482      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: irrflConcrete1 
19488      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.51ms 
19491      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_irrflConcrete2.proof 
19492      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 391.9ns 
19494      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
21955      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.46s 
21955      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: irrflConcrete2 
22815      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: irrflConcrete2 
22821      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.41ms 
22824      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_cancel_gtPos.proof 
22825      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 581.8ns 
22826      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
25304      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.48s 
25305      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: cancel_gtPos 
26146      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: cancel_gtPos 
26207      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 56.92ms 
26217      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_cancel_gtNeg.proof 
26218      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 821ns 
26219      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
28692      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.47s 
28693      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: cancel_gtNeg 
29507      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: cancel_gtNeg 
29530      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 19.61ms 
29536      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intRulesIgnoringOF/Taclet_moduloIntIsInInt.proof 
29537      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 246.5ns 
29538      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
32033      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.5s 
32034      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: moduloIntIsInInt 
32876      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: moduloIntIsInInt 
32880      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 740.4ns 
32883      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intRulesIgnoringOF/Taclet_moduloLongIsInLong.proof 
32883      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 366.9ns 
32884      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
35305      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.42s 
35306      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: moduloLongIsInLong 
36105      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: moduloLongIsInLong 
36108      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 588.1ns 
36116      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intRulesIgnoringOF/Taclet_moduloShortIsInShort.proof 
36117      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 225.3ns 
36118      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
38538      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.42s 
38539      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: moduloShortIsInShort 
39295      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: moduloShortIsInShort 
39298      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 602.7ns 
39301      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intRulesIgnoringOF/Taclet_moduloByteIsInByte.proof 
39301      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 369.4ns 
39302      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
41732      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.43s 
41732      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: moduloByteIsInByte 
42508      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: moduloByteIsInByte 
42511      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 655.1ns 
42514      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intRulesIgnoringOF/Taclet_moduloCharIsInChar.proof 
42514      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 220.3ns 
42515      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
44893      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.38s 
44894      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: moduloCharIsInChar 
45689      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: moduloCharIsInChar 
45692      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 674ns 
45695      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_div_unique1.proof 
45695      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 601.1ns 
45697      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
48095      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.4s 
48095      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: div_unique1 
48891      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: div_unique1 
48969      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 67.97ms 
48971      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_div_unique2.proof 
48971      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 129.9ns 
48972      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
51377      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.41s 
51377      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: div_unique2 
52150      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: div_unique2 
52176      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 22.79ms 
52178      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_div_exists.proof 
52179      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 151.7ns 
52180      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
54557      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.38s 
54558      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: div_exists 
55322      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: div_exists 
55503      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 171.5ms 
55506      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_div_one.proof 
55506      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 156.6ns 
55507      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
57886      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.38s 
57887      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: div_one 
58664      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: div_one 
58671      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.43ms 
58674      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdiv_one.proof 
58674      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 167.4ns 
58675      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
61070      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.4s 
61072      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdiv_one 
61825      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdiv_one 
61828      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.21ms 
61839      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_div_zero.proof 
61840      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 989.1ns 
61842      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
64270      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.43s 
64270      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: div_zero 
65040      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: div_zero 
65075      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 30.02ms 
65076      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divResZero1.proof 
65077      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 134.3ns 
65077      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
67455      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.38s 
67455      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divResZero1 
68230      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divResZero1 
68242      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 8.62ms 
68243      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divResZero2.proof 
68244      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 117.1ns 
68244      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
70640      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.4s 
70640      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divResZero2 
71414      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divResZero2 
71425      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 7.88ms 
71426      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divResOne1.proof 
71427      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 128ns 
71427      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
73783      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.36s 
73783      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divResOne1 
74555      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divResOne1 
74572      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 13.97ms 
74575      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divResOne2.proof 
74575      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 125.7ns 
74576      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
77096      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.52s 
77097      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divResOne2 
77851      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divResOne2 
77863      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 8.37ms 
77865      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_div_cancel1.proof 
77866      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 350.1ns 
77867      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
80248      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.38s 
80249      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: div_cancel1 
81027      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: div_cancel1 
81045      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 13.93ms 
81047      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_div_cancel2.proof 
81047      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 213.4ns 
81048      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
83412      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.36s 
83412      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: div_cancel2 
84193      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: div_cancel2 
84196      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.23ms 
84198      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divAddMultDenom.proof 
84198      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 195.8ns 
84199      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
86580      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.38s 
86581      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divAddMultDenom 
87343      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divAddMultDenom 
87373      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 24.77ms 
87376      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divMinus.proof 
87376      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 223.4ns 
87377      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
89729      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.35s 
89729      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divMinus 
90510      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divMinus 
90571      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 54.03ms 
90574      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divMinusDenom.proof 
90574      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 339.2ns 
90575      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
92937      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.36s 
92937      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divMinusDenom 
93699      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divMinusDenom 
93730      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 25.36ms 
93733      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divLeastDPos.proof 
93733      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 342.7ns 
93734      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
96050      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.32s 
96051      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divLeastDPos 
96809      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divLeastDPos 
96815      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.27ms 
96817      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divLeastDNeg.proof 
96818      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 274.99ns 
96819      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
99152      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.33s 
99152      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divLeastDNeg 
99889      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divLeastDNeg 
99900      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 8.38ms 
99901      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divGreatestDPos.proof 
99902      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 95.8ns 
99902      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
102230     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.33s 
102231     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divGreatestDPos 
102985     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divGreatestDPos 
102995     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 7.11ms 
102996     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divGreatestDNeg.proof 
102996     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 119ns 
102997     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
105314     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.32s 
105314     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divGreatestDNeg 
106093     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divGreatestDNeg 
106099     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.19ms 
106101     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divIncreasingPos.proof 
106101     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 95.4ns 
106101     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
108436     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.33s 
108436     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divIncreasingPos 
109201     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divIncreasingPos 
109209     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.21ms 
109210     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divIncreasingNeg.proof 
109210     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 103.4ns 
109211     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
111525     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.31s 
111525     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divIncreasingNeg 
112282     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divIncreasingNeg 
112293     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 8.46ms 
112294     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdiv_zero.proof 
112294     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 95ns 
112295     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
114631     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.34s 
114631     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdiv_zero 
115370     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdiv_zero 
115374     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.25ms 
115376     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdivPulloutMinusNum.proof 
115376     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 321.5ns 
115377     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
117693     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.32s 
117693     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdivPulloutMinusNum 
118453     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdivPulloutMinusNum 
118462     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 6.87ms 
118463     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdivPulloutMinusDenom.proof 
118463     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 107.2ns 
118465     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
120784     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.32s 
120784     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdivPulloutMinusDenom 
121541     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdivPulloutMinusDenom 
121574     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 28.06ms 
121576     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdiv_uniquePosPos.proof 
121576     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 97.5ns 
121577     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
123903     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.33s 
123903     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdiv_uniquePosPos 
124661     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdiv_uniquePosPos 
124683     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 16.65ms 
124685     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdiv_uniquePosNeg.proof 
124685     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 106.1ns 
124687     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
127008     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.32s 
127008     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdiv_uniquePosNeg 
127762     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdiv_uniquePosNeg 
127777     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 11.67ms 
127778     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdiv_uniqueNegPos.proof 
127779     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 100.7ns 
127779     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
130103     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.32s 
130103     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdiv_uniqueNegPos 
130856     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdiv_uniqueNegPos 
130872     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 12.27ms 
130873     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdiv_uniqueNegNeg.proof 
130873     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 107.2ns 
130874     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
133206     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.33s 
133206     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdiv_uniqueNegNeg 
133965     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdiv_uniqueNegNeg 
133980     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 11.43ms 
133981     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdivMultDenom1.proof 
133981     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 98.6ns 
133982     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
136326     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.34s 
136326     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdivMultDenom1 
137062     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdivMultDenom1 
137096     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 28.76ms 
137097     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdivMultDenom2.proof 
137097     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 84.4ns 
137098     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
139414     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.32s 
139414     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdivMultDenom2 
140165     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdivMultDenom2 
140168     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.01ms 
140169     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_mod_geZero.proof 
140169     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 85.2ns 
140170     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
142477     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.31s 
142477     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: mod_geZero 
143234     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: mod_geZero 
143238     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.11ms 
143240     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_mod_lessDenom.proof 
143240     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 92ns 
143240     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
145581     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.34s 
145581     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: mod_lessDenom 
146344     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: mod_lessDenom 
146352     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 5.3ms 
146353     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmod_NumPos.proof 
146353     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 84.6ns 
146354     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
148665     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.31s 
148665     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmod_NumPos 
149417     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmod_NumPos 
149424     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 5.01ms 
149426     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmod_NumNeg.proof 
149426     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 83.7ns 
149427     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
151744     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.32s 
151744     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmod_NumNeg 
152475     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmod_NumNeg 
152492     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 13.43ms 
152493     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmod_geZero.proof 
152493     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 89.6ns 
152494     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
154815     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.32s 
154816     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmod_geZero 
155569     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmod_geZero 
155576     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 5.19ms 
155578     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmodNumZero.proof 
155578     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 83.9ns 
155579     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
157899     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.32s 
157899     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmodNumZero 
158637     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmodNumZero 
158641     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.34ms 
158643     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmod_pulloutminusNum.proof 
158643     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 257.6ns 
158644     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
160981     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.34s 
160982     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmod_pulloutminusNum 
161742     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmod_pulloutminusNum 
161746     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.49ms 
161748     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmod_pulloutminusDenom.proof 
161749     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 266.6ns 
161750     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
164053     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.3s 
164054     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmod_pulloutminusDenom 
164825     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmod_pulloutminusDenom 
164829     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.86ms 
164832     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmodUnique1.proof 
164832     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 292.5ns 
164833     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
167181     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.35s 
167181     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmodUnique1 
167935     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmodUnique1 
167993     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 49.44ms 
167994     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmodUnique2.proof 
167994     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 89.9ns 
167995     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
170317     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.32s 
170317     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmodUnique2 
171080     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmodUnique2 
171146     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 57.83ms 
171148     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_intDivRem.proof 
171148     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 108.6ns 
171149     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
173472     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.32s 
173472     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: intDivRem 
174206     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: intDivRem 
174209     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.45ms 
174210     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmodjmod.proof 
174210     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 94.2ns 
174211     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
176532     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.32s 
176532     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmodjmod 
177288     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmodjmod 
177334     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 42.07ms 
177339     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmodDivisible.proof 
177345     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 6.08ms 
177346     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
179660     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.31s 
179660     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmodDivisible 
180422     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmodDivisible 
180442     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 16.74ms 
180445     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmodDivisibleRep.proof 
180445     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 258.5ns 
180446     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
182762     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.32s 
182762     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmodDivisibleRep 
183509     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmodDivisibleRep 
183512     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 881.6ns 
183513     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdivAddMultDenom.proof 
183513     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 54.7ns 
183514     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
185803     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.29s 
185803     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdivAddMultDenom 
186573     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdivAddMultDenom 
186674     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 89.61ms 
186677     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmodAltZero.proof 
186677     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 236.8ns 
186678     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
189002     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.32s 
189002     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmodAltZero 
189750     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmodAltZero 
189758     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 6.33ms 
189760     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmodAddMultDenomZero.proof 
189760     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 70.2ns 
189760     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
192065     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.3s 
192065     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmodAddMultDenomZero 
192814     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmodAddMultDenomZero 
192820     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.9ms 
192821     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_polyDiv_zero.proof 
192821     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 77.9ns 
192822     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
195146     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.32s 
195147     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: polyDiv_zero 
195879     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: polyDiv_zero 
195892     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 10.21ms 
195893     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_polyMod_ltdivDenom.proof 
195893     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 73.6ns 
195894     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
198184     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.29s 
198184     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: polyMod_ltdivDenom 
198927     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: polyMod_ltdivDenom 
198936     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.92ms 
198938     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_empty.proof 
198938     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 56.4ns 
198939     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
201224     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.29s 
201224     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_empty 
201970     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_empty 
201973     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.39ms 
201975     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_induction_upper.proof 
201975     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 76ns 
201975     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
204289     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.31s 
204289     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_upper 
205045     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_induction_upper 
205048     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.94ms 
205050     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_induction_lower.proof 
205050     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 63.3ns 
205051     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
207342     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.29s 
207342     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_lower 
208090     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_induction_lower 
208103     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 10.57ms 
208104     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_bounds.proof 
208104     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 65ns 
208105     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
210400     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.29s 
210400     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_bounds 
211150     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_bounds 
211161     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 8.57ms 
211162     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_bounds2.proof 
211162     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 66.2ns 
211163     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
213438     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.27s 
213438     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_bounds2 
214182     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_bounds2 
214193     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 8.29ms 
214194     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_induction_upper2.proof 
214194     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 62.4ns 
214195     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
216487     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.29s 
216487     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_upper2 
217214     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_induction_upper2 
217217     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 950.79ns 
217218     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_induction_upper_concrete.proof 
217218     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 62.2ns 
217219     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
219510     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.29s 
219510     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_upper_concrete 
220262     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_induction_upper_concrete 
220265     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.33ms 
220267     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_induction_upper_concrete_2.proof 
220267     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 250.3ns 
220268     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
222548     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.28s 
222548     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_upper_concrete_2 
223295     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_induction_upper_concrete_2 
223300     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.39ms 
223301     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_induction_upper2_concrete.proof 
223301     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 56.5ns 
223301     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
225594     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.29s 
225594     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_upper2_concrete 
226342     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_induction_upper2_concrete 
226344     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 861.39ns 
226346     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_induction_lower_concrete.proof 
226346     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 251.3ns 
226347     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
228644     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.3s 
228644     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_lower_concrete 
229393     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_induction_lower_concrete 
229394     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 441ns 
229396     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_induction_lower2.proof 
229396     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 55.1ns 
229396     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
231692     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.3s 
231692     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_lower2 
232421     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_induction_lower2 
232424     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.53ms 
232425     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_induction_lower2_concrete.proof 
232425     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 65.3ns 
232426     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
234720     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.29s 
234720     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_lower2_concrete 
235469     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_induction_lower2_concrete 
235472     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 675.2ns 
235474     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_positive.proof 
235474     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 215ns 
235475     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
237760     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.29s 
237760     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_positive 
238508     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_positive 
238542     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 31.26ms 
238544     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_upper_bound.proof 
238544     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 189.1ns 
238545     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
240853     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.31s 
240853     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_upper_bound 
241602     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_upper_bound 
241631     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 26ms 
241634     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_lower_bound.proof 
241634     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 188.4ns 
241635     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
243928     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.29s 
243928     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_lower_bound 
244675     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_lower_bound 
244694     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 16.29ms 
244696     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_positive_lower_bound_element.proof 
244696     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 225.3ns 
244697     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
246988     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.29s 
246988     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_positive_lower_bound_element 
247732     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_positive_lower_bound_element 
247760     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 23.46ms 
247762     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_sub_same_index.proof 
247762     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 193.5ns 
247763     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
250044     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.28s 
250044     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_sub_same_index 
250790     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_sub_same_index 
250808     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 14.29ms 
250809     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_less_same_index.proof 
250809     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 53.1ns 
250810     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
253096     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.29s 
253096     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_less_same_index 
253835     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_less_same_index 
253867     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 27.84ms 
253869     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_equal_except_one_index.proof 
253869     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 194ns 
253870     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
256167     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.3s 
256167     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_equal_except_one_index 
256910     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_equal_except_one_index 
256926     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 12.67ms 
256927     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_is_max.proof 
256927     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 64.8ns 
256928     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
259211     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.28s 
259211     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_is_max 
259969     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_is_max 
259982     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 10.03ms 
259983     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_is_max2.proof 
259984     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 65.2ns 
259984     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
262327     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.34s 
262327     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_is_max2 
263090     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_is_max2 
263105     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 12.15ms 
263108     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_is_max3.proof 
263108     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 230.7ns 
263109     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
265441     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.33s 
265441     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_is_max3 
266195     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_is_max3 
266207     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 9.54ms 
266209     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_is_max4.proof 
266209     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 103.2ns 
266210     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
268526     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.32s 
268526     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_is_max4 
269281     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_is_max4 
269297     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 13.15ms 
269298     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_lt_max.proof 
269298     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 53.9ns 
269299     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
271605     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.31s 
271605     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_lt_max 
272355     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_lt_max 
272370     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 12.31ms 
272372     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_lt_max2.proof 
272372     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 72.5ns 
272372     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
274682     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.31s 
274683     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_lt_max2 
275420     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_lt_max2 
275436     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 12.8ms 
275438     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_lt_max3.proof 
275438     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 67.9ns 
275439     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
277769     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.33s 
277769     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_lt_max3 
278520     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_lt_max3 
278535     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 11.52ms 
278536     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_lt_max4.proof 
278536     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 93.1ns 
278537     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
280835     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.3s 
280835     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_lt_max4 
281593     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_lt_max4 
281606     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 10.74ms 
281607     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_gt0.proof 
281607     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 68.9ns 
281608     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
283933     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.32s 
283933     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_gt0 
284685     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_gt0 
284701     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 13.58ms 
284702     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_gt0_alt.proof 
284703     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 65.8ns 
284703     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
286995     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.29s 
286995     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_gt0_alt 
287746     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_gt0_alt 
287761     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 12.34ms 
287762     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_add_concrete.proof 
287762     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 66.7ns 
287763     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
290080     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.32s 
290080     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_add_concrete 
290810     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_add_concrete 
290816     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.36ms 
290817     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bprod/Taclet_bprod_all_positive.proof 
290817     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 50.1ns 
290818     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
293129     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.31s 
293129     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bprod_all_positive 
293882     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bprod_all_positive 
293893     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 7.95ms 
293894     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bprod/Taclet_bprod_split.proof 
293894     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 52.6ns 
293895     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
296213     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.32s 
296213     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bprod_split 
296946     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bprod_split 
296950     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.62ms 
296951     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powConcrete0.proof 
296951     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 64.1ns 
296952     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
299288     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.34s 
299288     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powConcrete0 
300047     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powConcrete0 
300049     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 511.1ns 
300050     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powConcrete1.proof 
300050     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 59.9ns 
300051     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
302361     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.31s 
302361     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powConcrete1 
303125     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powConcrete1 
303128     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 666.1ns 
303130     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powSplitFactor.proof 
303130     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 191.5ns 
303131     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
305458     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.33s 
305458     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powSplitFactor 
306212     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powSplitFactor 
306219     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.69ms 
306222     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powAdd.proof 
306222     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 70ns 
306222     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
308540     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.32s 
308540     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powAdd 
309302     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powAdd 
309308     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.84ms 
309309     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powMono.proof 
309309     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 55.4ns 
309310     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
311658     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.35s 
311658     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powMono 
312397     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powMono 
312406     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 7.06ms 
312407     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powMonoConcrete.proof 
312407     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 62.3ns 
312408     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
314732     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.32s 
314732     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powMonoConcrete 
315484     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powMonoConcrete 
315487     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.55ms 
315489     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powMonoConcreteRight.proof 
315489     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 50ns 
315489     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
317806     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.32s 
317806     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powMonoConcreteRight 
318568     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powMonoConcreteRight 
318570     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 444.9ns 
318571     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powPositive.proof 
318571     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 60.8ns 
318572     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
320913     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.34s 
320913     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powPositive 
321666     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powPositive 
321671     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.95ms 
321672     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powPositiveConcrete.proof 
321672     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 65.3ns 
321672     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
323977     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.3s 
323977     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powPositiveConcrete 
324730     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powPositiveConcrete 
324732     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 557.9ns 
324733     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powGeq1Concrete.proof 
324733     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 57.2ns 
324734     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
327036     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.3s 
327036     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powGeq1Concrete 
327772     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powGeq1Concrete 
327774     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 462.8ns 
327775     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_pow2InIntLower.proof 
327775     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 56.6ns 
327776     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
330087     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.31s 
330088     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: pow2InIntLower 
330842     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: pow2InIntLower 
330844     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 485.5ns 
330845     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_pow2InIntUpper.proof 
330845     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 58ns 
330846     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
333165     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.32s 
333165     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: pow2InIntUpper 
333900     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: pow2InIntUpper 
333903     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.62ms 
333904     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logSelfConcrete.proof 
333904     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 60.9ns 
333905     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
336239     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.33s 
336239     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logSelfConcrete 
336994     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logSelfConcrete 
337000     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.45ms 
337002     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_log1Concrete.proof 
337002     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 49.9ns 
337002     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
339352     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.35s 
339352     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: log1Concrete 
340107     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: log1Concrete 
340110     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.49ms 
340112     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logProduct.proof 
340113     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 244.8ns 
340113     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
342438     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.32s 
342438     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logProduct 
343191     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logProduct 
343197     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.47ms 
343198     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logTimesBaseConcrete.proof 
343198     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 62.1ns 
343198     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
345488     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.29s 
345488     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logTimesBaseConcrete 
346239     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logTimesBaseConcrete 
346243     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.79ms 
346244     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logProdIdentity.proof 
346244     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 63.3ns 
346245     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
348556     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.31s 
348556     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logProdIdentity 
349309     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logProdIdentity 
349321     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 9.04ms 
349322     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logProdIdentityConcrete.proof 
349322     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 62.7ns 
349323     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
351617     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.29s 
351617     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logProdIdentityConcrete 
352370     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logProdIdentityConcrete 
352373     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.04ms 
352375     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logPowIdentity.proof 
352375     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 60.5ns 
352375     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
354702     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.33s 
354702     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logPowIdentity 
355454     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logPowIdentity 
355457     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 974.8ns 
355458     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logPowIdentityConcrete.proof 
355458     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 49.5ns 
355459     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
357758     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.3s 
357758     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logPowIdentityConcrete 
358513     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logPowIdentityConcrete 
358516     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.63ms 
358518     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logPositive.proof 
358518     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 68.6ns 
358518     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
360853     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.33s 
360853     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logPositive 
361608     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logPositive 
361621     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 10.28ms 
361622     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logPositiveConcrete.proof 
361622     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 62.9ns 
361623     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
363965     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.34s 
363965     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logPositiveConcrete 
364704     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logPositiveConcrete 
364708     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 342.9ns 
364710     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logMono.proof 
364710     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 69.6ns 
364711     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
367051     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.34s 
367051     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logMono 
367808     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logMono 
367835     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 22.07ms 
367836     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logMonoConcrete.proof 
367836     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 74.1ns 
367837     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
370187     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.35s 
370187     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logMonoConcrete 
370928     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logMonoConcrete 
370931     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.5ms 
370932     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powLogLess.proof 
370932     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 58.5ns 
370933     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
373273     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.34s 
373273     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powLogLess 
374035     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powLogLess 
374051     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 12.2ms 
374053     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powLogMore2.proof 
374053     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 199.6ns 
374054     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
376406     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.35s 
376406     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powLogMore2 
377164     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powLogMore2 
377178     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 11.46ms 
377180     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logLessThanPow.proof 
377180     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 61.3ns 
377181     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
379514     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.33s 
379514     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logLessThanPow 
380277     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logLessThanPow 
380295     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 14.66ms 
380297     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logLessThanPowConcrete.proof 
380297     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 73.2ns 
380297     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
382687     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.39s 
382687     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logLessThanPowConcrete 
383447     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logLessThanPowConcrete 
383450     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 477.5ns 
383451     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logSqueeze.proof 
383451     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 52.8ns 
383452     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
385810     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.36s 
385810     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logSqueeze 
386570     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logSqueeze 
386574     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.06ms 
386576     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/booleanRules/Taclet_ifthenelse_equals.proof 
386576     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 60.2ns 
386577     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
388903     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.33s 
388903     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: ifthenelse_equals 
389661     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: ifthenelse_equals 
389665     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.39ms 
389666     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/booleanRules/Taclet_ifthenelse_equals_1.proof 
389666     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 61.2ns 
389667     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
391997     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.33s 
391997     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: ifthenelse_equals_1 
392755     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: ifthenelse_equals_1 
392758     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 729.2ns 
392759     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/booleanRules/Taclet_ifthenelse_equals_2.proof 
392759     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 50.4ns 
392760     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
395095     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.34s 
395095     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: ifthenelse_equals_2 
395858     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: ifthenelse_equals_2 
395861     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 758.7ns 
395862     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/locSet/Taclet_disjointWithSingleton1.proof 
395862     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 61.6ns 
395863     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
398180     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.32s 
398180     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: disjointWithSingleton1 
398968     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: disjointWithSingleton1 
398972     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.23ms 
398973     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/locSet/Taclet_disjointWithSingleton2.proof 
398973     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 61.4ns 
398974     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
401399     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.43s 
401400     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: disjointWithSingleton2 
402192     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: disjointWithSingleton2 
402195     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.09ms 
402196     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/locSet/Taclet_disjointArrayRanges.proof 
402196     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 58.6ns 
402197     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
404552     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.36s 
404553     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: disjointArrayRanges 
405313     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: disjointArrayRanges 
405320     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.98ms 
405321     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/locSet/Taclet_disjointArrayRangeAllFields1.proof 
405322     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 65.1ns 
405322     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
407639     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.32s 
407640     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: disjointArrayRangeAllFields1 
408400     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: disjointArrayRangeAllFields1 
408406     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.38ms 
408408     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/locSet/Taclet_disjointArrayRangeAllFields2.proof 
408408     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 57.3ns 
408409     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
410737     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.33s 
410737     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: disjointArrayRangeAllFields2 
411499     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: disjointArrayRangeAllFields2 
411508     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 6.51ms 
411509     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqSelfDefinition.proof 
411509     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 64.8ns 
411510     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
413843     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.33s 
413843     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqSelfDefinition 
414609     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqSelfDefinition 
414616     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 5.36ms 
414617     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqOutsideValue.proof 
414617     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 61ns 
414618     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
416954     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.34s 
416955     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqOutsideValue 
417719     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqOutsideValue 
417723     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.05ms 
417724     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_castedGetAny.proof 
417724     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 72.7ns 
417725     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
420039     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.31s 
420039     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: castedGetAny 
420806     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: castedGetAny 
420810     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.26ms 
420811     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqGetAlphaCast.proof 
420812     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 65.7ns 
420812     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
423155     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.34s 
423155     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqGetAlphaCast 
423921     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqGetAlphaCast 
423923     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 712.5ns 
423924     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqSingleton.proof 
423924     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 63.1ns 
423925     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
426263     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.34s 
426263     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqSingleton 
427030     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqSingleton 
427033     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 874.2ns 
427034     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqSingletonConcrete.proof 
427034     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 60.3ns 
427034     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
429371     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.34s 
429371     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqSingletonConcrete 
430138     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqSingletonConcrete 
430141     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 780.4ns 
430142     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqConcat.proof 
430142     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 66.6ns 
430143     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
432485     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.34s 
432485     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqConcat 
433256     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqConcat 
433266     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 7.97ms 
433273     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqSub.proof 
433273     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 213.8ns 
433274     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
435621     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.35s 
435621     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqSub 
436395     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqSub 
436397     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.13ms 
436399     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqReverse.proof 
436399     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 67.5ns 
436400     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
438749     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.35s 
438750     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqReverse 
439522     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqReverse 
439527     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.56ms 
439529     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqEmpty.proof 
439529     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 72.1ns 
439530     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
441902     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.37s 
441903     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqEmpty 
442675     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqEmpty 
442678     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 808.4ns 
442679     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqSingleton.proof 
442679     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 63.3ns 
442680     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
445043     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.36s 
445043     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqSingleton 
445811     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqSingleton 
445813     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 574.2ns 
445815     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqConcat.proof 
445815     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 59.4ns 
445815     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
448155     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.34s 
448155     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqConcat 
448925     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqConcat 
448928     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.33ms 
448929     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqSub.proof 
448930     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 71.5ns 
448930     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
451281     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.35s 
451282     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqSub 
452048     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqSub 
452051     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 769.3ns 
452052     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqReverse.proof 
452052     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 53.7ns 
452053     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
454401     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.35s 
454401     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqReverse 
455167     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqReverse 
455170     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 981.2ns 
455171     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_equalityToSeqGetAndSeqLenLeft.proof 
455171     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 63.1ns 
455172     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
457513     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.34s 
457513     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: equalityToSeqGetAndSeqLenLeft 
458282     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: equalityToSeqGetAndSeqLenLeft 
458284     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 974.3ns 
458286     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_equalityToSeqGetAndSeqLenRight.proof 
458286     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 120.8ns 
458287     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
460641     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.35s 
460641     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: equalityToSeqGetAndSeqLenRight 
461391     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: equalityToSeqGetAndSeqLenRight 
461395     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.92ms 
461396     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqSingletonEQ.proof 
461396     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 57.2ns 
461397     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
463758     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.36s 
463758     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqSingletonEQ 
464507     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqSingletonEQ 
464509     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 742.5ns 
464510     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqConcatEQ.proof 
464511     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 59.7ns 
464512     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
466856     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.34s 
466856     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqConcatEQ 
467627     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqConcatEQ 
467635     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 6.24ms 
467637     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqSubEQ.proof 
467637     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 59.8ns 
467638     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
469991     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.35s 
469991     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqSubEQ 
470761     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqSubEQ 
470763     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 606.3ns 
470764     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqReverseEQ.proof 
470764     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 65.6ns 
470765     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
473099     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.33s 
473100     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqReverseEQ 
473869     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqReverseEQ 
473875     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.35ms 
473876     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqEmptyEQ.proof 
473876     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 53.1ns 
473877     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
476221     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.34s 
476222     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqEmptyEQ 
476988     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqEmptyEQ 
476991     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 799.6ns 
476992     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqSingletonEQ.proof 
476992     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 82.6ns 
476993     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
479333     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.34s 
479333     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqSingletonEQ 
480101     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqSingletonEQ 
480103     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 719.9ns 
480105     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqConcatEQ.proof 
480105     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 58.3ns 
480105     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
482448     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.34s 
482448     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqConcatEQ 
483217     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqConcatEQ 
483220     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.85ms 
483221     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqSubEQ.proof 
483221     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 55.4ns 
483222     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
485591     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.37s 
485592     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqSubEQ 
486348     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqSubEQ 
486350     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 985.8ns 
486351     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqReverseEQ.proof 
486351     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 64.5ns 
486352     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
488716     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.36s 
488717     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqReverseEQ 
489485     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqReverseEQ 
489488     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.19ms 
489489     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqDefEQ.proof 
489489     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 64.4ns 
489490     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
491837     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.35s 
491837     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqDefEQ 
492603     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqDefEQ 
492606     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 980.7ns 
492607     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqDefEQ.proof 
492607     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 62.5ns 
492608     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
494951     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.34s 
494951     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqDefEQ 
495720     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqDefEQ 
495724     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.95ms 
495725     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqConcatWithSeqEmpty1.proof 
495725     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 63.7ns 
495726     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
498061     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.34s 
498061     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqConcatWithSeqEmpty1 
498831     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqConcatWithSeqEmpty1 
498838     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 5.1ms 
498839     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqConcatWithSeqEmpty2.proof 
498839     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 66.6ns 
498840     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
501184     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.34s 
501184     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqConcatWithSeqEmpty2 
501954     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqConcatWithSeqEmpty2 
501961     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 5.59ms 
501963     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqReverseOfSeqEmpty.proof 
501963     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 69.7ns 
501963     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
504330     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.37s 
504330     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqReverseOfSeqEmpty 
505098     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqReverseOfSeqEmpty 
505104     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.07ms 
505105     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_subSeqComplete.proof 
505105     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 56.8ns 
505106     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
507441     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.34s 
507441     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: subSeqComplete 
508207     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: subSeqComplete 
508213     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.99ms 
508214     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_subSeqTailR.proof 
508214     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 65.6ns 
508215     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
510557     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.34s 
510557     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: subSeqTailR 
511328     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: subSeqTailR 
511338     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 7.5ms 
511339     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_subSeqTailL.proof 
511339     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 89.1ns 
511340     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
513703     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.36s 
513703     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: subSeqTailL 
514470     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: subSeqTailL 
514480     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 7.45ms 
514481     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_subSeqTailEQR.proof 
514481     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 67.8ns 
514482     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
516825     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.34s 
516825     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: subSeqTailEQR 
517600     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: subSeqTailEQR 
517610     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 7.21ms 
517611     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_subSeqTailEQL.proof 
517611     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 72ns 
517612     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
519956     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.34s 
519956     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: subSeqTailEQL 
520725     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: subSeqTailEQL 
520731     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.7ms 
520733     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDef_split.proof 
520733     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 62.6ns 
520734     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
523066     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.33s 
523066     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_split 
523836     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDef_split 
523855     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 15.83ms 
523856     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDef_induction_upper.proof 
523856     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 65.5ns 
523857     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
526192     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.34s 
526192     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_induction_upper 
526963     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDef_induction_upper 
527019     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 52.45ms 
527021     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDef_induction_upper_concrete.proof 
527021     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 192.1ns 
527022     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
529359     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.34s 
529359     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_induction_upper_concrete 
530127     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDef_induction_upper_concrete 
530148     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 17.13ms 
530149     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDef_induction_lower.proof 
530149     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 68.5ns 
530150     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
532485     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.34s 
532486     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_induction_lower 
533254     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDef_induction_lower 
533272     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 14.9ms 
533274     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDef_induction_lower_concrete.proof 
533274     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 67.7ns 
533275     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
535603     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.33s 
535603     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_induction_lower_concrete 
536370     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDef_induction_lower_concrete 
536389     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 15.3ms 
536390     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDef_split_in_three.proof 
536390     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 55.1ns 
536391     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
538737     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.35s 
538737     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_split_in_three 
539500     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDef_split_in_three 
539547     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 38.57ms 
539548     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDef_empty.proof 
539549     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 66.4ns 
539549     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
541876     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.33s 
541876     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_empty 
542643     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDef_empty 
542653     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 8.21ms 
542654     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDef_one_summand.proof 
542654     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 54.7ns 
542655     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
544992     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.34s 
544993     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_one_summand 
545761     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDef_one_summand 
545766     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.85ms 
545768     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDef_lower_equals_upper.proof 
545768     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 217.4ns 
545769     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
548113     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.34s 
548113     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_lower_equals_upper 
548878     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDef_lower_equals_upper 
548882     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.77ms 
548883     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDefOfSeq.proof 
548883     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 51.8ns 
548883     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
551220     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.34s 
551220     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDefOfSeq 
551985     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDefOfSeq 
551997     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 9.15ms 
551998     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqSelfDefinitionEQ2.proof 
551998     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 63.6ns 
551999     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
554347     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.35s 
554347     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqSelfDefinitionEQ2 
555112     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqSelfDefinitionEQ2 
555118     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.9ms 
555119     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_indexOfSeqSingleton.proof 
555119     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 56.3ns 
555120     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
557444     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.32s 
557444     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: indexOfSeqSingleton 
558208     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: indexOfSeqSingleton 
558211     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.25ms 
558212     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_indexOfSeqConcatFirst.proof 
558212     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 59.3ns 
558213     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
560548     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.33s 
560548     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: indexOfSeqConcatFirst 
561315     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: indexOfSeqConcatFirst 
561324     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 7.39ms 
561326     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_indexOfSeqConcatSecond.proof 
561326     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 67ns 
561326     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
563673     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.35s 
563674     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: indexOfSeqConcatSecond 
564438     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: indexOfSeqConcatSecond 
564448     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 7.67ms 
564450     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_indexOfSeqSub.proof 
564450     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 55ns 
564450     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
566790     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.34s 
566790     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: indexOfSeqSub 
567557     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: indexOfSeqSub 
567570     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 10.08ms 
567572     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfArray2seq.proof 
567572     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 202.7ns 
567573     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
569935     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.36s 
569935     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfArray2seq 
570701     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfArray2seq 
570704     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 933.1ns 
570705     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getAnyOfArray2seq.proof 
570705     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 53.3ns 
570706     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
573043     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.34s 
573043     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getAnyOfArray2seq 
573808     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getAnyOfArray2seq 
573812     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.62ms 
573813     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfArray2seq.proof 
573813     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 77.9ns 
573814     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
576177     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.36s 
576177     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfArray2seq 
576944     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfArray2seq 
576949     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.74ms 
576950     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_getAnyOfNPermInv.proof 
576951     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 67ns 
576951     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
579292     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.34s 
579292     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getAnyOfNPermInv 
580059     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getAnyOfNPermInv 
580064     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.74ms 
580065     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqNPermRange.proof 
580065     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 54.4ns 
580066     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
582431     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.37s 
582431     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqNPermRange 
583196     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqNPermRange 
583237     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 34.82ms 
583238     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermTrans.proof 
583238     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 66.5ns 
583239     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
585582     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.34s 
585582     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermTrans 
586354     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermTrans 
586374     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 16.5ms 
586376     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermRefl.proof 
586376     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 208.1ns 
586377     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
588766     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.39s 
588767     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermRefl 
589542     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermRefl 
589553     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 8.94ms 
589554     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermSplit.proof 
589554     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 72.8ns 
589555     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
591946     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.39s 
591946     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermSplit 
592722     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermSplit 
592725     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 310.6ns 
592726     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqNPermRight.proof 
592726     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 62.9ns 
592727     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
595115     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.39s 
595115     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqNPermRight 
595891     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqNPermRight 
595972     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 69.09ms 
595974     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermFromSwap.proof 
595974     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 64.3ns 
595974     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
598366     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.39s 
598367     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermFromSwap 
599149     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermFromSwap 
599183     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 29.83ms 
599185     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermTransAlt0.proof 
599185     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 64.4ns 
599185     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
601573     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.39s 
601573     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermTransAlt0 
602350     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermTransAlt0 
602352     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 339ns 
602354     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermTransAlt1.proof 
602355     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 77.7ns 
602357     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
604729     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.37s 
604729     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermTransAlt1 
605506     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermTransAlt1 
605508     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 247.2ns 
605509     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermTransAlt2.proof 
605509     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 75.4ns 
605510     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
607903     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.39s 
607903     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermTransAlt2 
608681     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermTransAlt2 
608683     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 232.3ns 
608685     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermTransAlt3.proof 
608685     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 58.1ns 
608686     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
611072     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.39s 
611072     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermTransAlt3 
611850     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermTransAlt3 
611852     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 408.2ns 
611854     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermForall.proof 
611854     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 76.8ns 
611854     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
614258     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.4s 
614258     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermForall 
615074     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermForall 
615166     INFO  Test worker     d.u.i.k.s.SMTFocusResults Analyzing unsat core: (L_1 L_3 L_4) 
615174     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 97.45ms 
615176     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermExists.proof 
615176     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 98ns 
615177     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
617589     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.41s 
617589     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermExists 
618367     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermExists 
618413     INFO  Test worker     d.u.i.k.s.SMTFocusResults Analyzing unsat core: (L_1 L_3 L_5 L_6 L_7) 
618414     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 44.48ms 
618415     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm2/Taclet_schiffl_lemma_2.proof 
618415     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 63.1ns 
618417     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
620794     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.38s 
620794     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: schiffl_lemma_2 
621571     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: schiffl_lemma_2 
621573     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3ns 
621602     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [1] goal: 0, source line: 49, command: 'macro split-prop' 
621660     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [2] goal: 3, source line: 50, command: 'rule allRight' 
621675     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [3] goal: 4, source line: 51, command: 'rule allRight' 
621683     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [4] goal: 5, source line: 52, command: 'macro split-prop' 
621698     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [5] goal: 11, source line: 53, command: 'rule 'seqPermDefLeft'' 
621699     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [6] goal: 12, source line: 54, command: 'rule 'andLeft'' 
621701     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [7] goal: 13, source line: 55, command: 'rule 'exLeft'' 
621703     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [8] goal: 14, source line: 56, command: 'macro split-prop' 
621709     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [9] goal: 16, source line: 57, command: 'rule  seqNPermRange' 
621713     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' 
621716     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [11] goal: 18, source line: 60, command: 'rule impLeft' 
621720     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [12] goal: 19, source line: 61, command: 'tryclose branch' 
621974     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [13] goal: 20, source line: 62, command: 'rule andLeft' 
621975     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [14] goal: 97, source line: 63, command: 'rule andLeft' 
621978     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' 
621979     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [16] goal: 99, source line: 66, command: 'rule impLeft' 
621981     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [17] goal: 100, source line: 67, command: 'tryclose branch' 
622118     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [18] goal: 101, source line: 68, command: 'rule andLeft' 
622119     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [19] goal: 188, source line: 69, command: 'rule andLeft' 
622123     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [20] goal: 189, source line: 70, command: 'rule seqNPermDefLeft' 
622124     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' 
622125     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [22] goal: 191, source line: 73, command: 'rule impLeft' 
622127     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [23] goal: 192, source line: 74, command: 'tryclose branch' 
622293     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [24] goal: 193, source line: 75, command: 'rule exLeft' 
622296     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [25] goal: 310, source line: 76, command: 'rule andLeft' 
622298     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [26] goal: 311, source line: 77, command: 'rule andLeft' 
622299     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' 
622305     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [28] goal: 313, source line: 80, command: 'rule impLeft' 
622307     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [29] goal: 314, source line: 81, command: 'tryclose branch' 
622411     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [30] goal: 315, source line: 82, command: 'rule exLeft' 
622411     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [31] goal: 420, source line: 83, command: 'rule andLeft' 
622413     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [32] goal: 421, source line: 84, command: 'rule andLeft' 
622413     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' 
622414     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [34] goal: 423, source line: 87, command: 'rule impLeft' 
622415     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [35] goal: 424, source line: 88, command: 'tryclose branch' 
622421     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [36] goal: 425, source line: 89, command: 'rule andLeft' 
622422     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [37] goal: 434, source line: 90, command: 'rule andLeft' 
622424     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' 
622424     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' 
622425     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [40] goal: 437, source line: 94, command: 'rule impLeft' 
622426     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [41] goal: 438, source line: 95, command: 'tryclose branch' 
622432     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [42] goal: 439, source line: 96, command: 'rule andLeft' 
622433     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [43] goal: 448, source line: 97, command: 'rule andLeft' 
622434     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' 
622435     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [45] goal: 450, source line: 99, command: 'instantiate var=iv  with='v_x_0'' 
622435     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [46] goal: 451, source line: 101, command: 'rule impLeft' 
622436     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [47] goal: 452, source line: 102, command: 'tryclose branch' 
622545     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [48] goal: 453, source line: 103, command: 'instantiate var=iv  with='v_y_0'' 
622545     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [49] goal: 562, source line: 105, command: 'rule impLeft' 
622546     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [50] goal: 563, source line: 106, command: 'tryclose branch' 
622676     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [51] goal: 564, source line: 107, command: 'cut 'v_x_0 = v_y_0'' 
622677     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)'' 
622678     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [53] goal: 676, source line: 111, command: 'rule andRight' 
622680     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [54] goal: 677, source line: 113, command: 'rule andRight' 
622680     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [55] goal: 679, source line: 114, command: 'rule andRight' 
622681     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [56] goal: 681, source line: 115, command: 'rule andRight' 
622681     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [57] goal: 683, source line: 116, command: 'rule lenOfSwap' 
622682     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [58] goal: 685, source line: 117, command: 'tryclose branch' 
622685     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [59] goal: 684, source line: 118, command: 'rule seqNPermSwapNPerm' 
622686     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' 
622687     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [61] goal: 688, source line: 121, command: 'instantiate hide var='jv' with='jv_0'' 
622688     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [62] goal: 689, source line: 122, command: 'rule impLeft' 
622688     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [63] goal: 690, source line: 123, command: 'tryclose branch' 
622776     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [64] goal: 691, source line: 124, command: 'tryclose branch' 
622779     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [65] goal: 682, source line: 125, command: 'rule allRight' 
622780     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [66] goal: 796, source line: 127, command: 'rule impRight' 
622781     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [67] goal: 797, source line: 128, command: 'rule andLeft' 
622782     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [68] goal: 798, source line: 129, command: 'instantiate var=iv with='v_iv_0'' 
622782     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [69] goal: 799, source line: 130, command: 'rule impLeft' 
622783     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [70] goal: 800, source line: 131, command: 'tryclose branch' 
622886     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [71] goal: 801, source line: 132, command: 'rule getOfSwap' 
622887     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [72] goal: 912, source line: 133, command: 'rule ifthenelse_negated' 
622888     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [73] goal: 913, source line: 134, command: 'rule ifthenelse_split occ=0' 
622889     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [74] goal: 914, source line: 135, command: 'rule andLeft' 
622890     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [75] goal: 916, source line: 136, command: 'rule andLeft' 
622891     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [76] goal: 917, source line: 137, command: 'rule andLeft' 
622891     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [77] goal: 918, source line: 138, command: 'rule ifthenelse_split occ=0' 
622892     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [78] goal: 919, source line: 139, command: 'tryclose branch' 
622978     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [79] goal: 920, source line: 140, command: 'rule ifthenelse_split occ=0' 
622979     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [80] goal: 1011, source line: 141, command: 'tryclose branch' 
623056     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [81] goal: 1012, source line: 142, command: 'tryclose branch' 
623060     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [82] goal: 915, source line: 143, command: 'tryclose branch' 
623064     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [83] goal: 680, source line: 144, command: 'rule getOfSwap' 
623066     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [84] goal: 1099, source line: 146, command: 'rule ifthenelse_negated' 
623067     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [85] goal: 1100, source line: 147, command: 'rule ifthenelse_split occ=0' 
623068     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [86] goal: 1101, source line: 148, command: 'rule andLeft' 
623069     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [87] goal: 1103, source line: 149, command: 'rule andLeft' 
623069     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [88] goal: 1104, source line: 150, command: 'rule andLeft' 
623070     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [89] goal: 1105, source line: 151, command: 'rule ifthenelse_split occ=0' 
623070     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [90] goal: 1106, source line: 152, command: 'tryclose branch' 
623077     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [91] goal: 1107, source line: 153, command: 'tryclose branch' 
623082     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [92] goal: 1102, source line: 154, command: 'tryclose branch' 
623161     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [93] goal: 678, source line: 155, command: 'rule getOfSwap' 
623162     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [94] goal: 1225, source line: 157, command: 'rule ifthenelse_negated' 
623164     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [95] goal: 1226, source line: 158, command: 'rule ifthenelse_split occ=0' 
623165     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [96] goal: 1227, source line: 159, command: 'rule andLeft' 
623165     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [97] goal: 1229, source line: 160, command: 'rule andLeft' 
623166     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [98] goal: 1230, source line: 161, command: 'rule andLeft' 
623166     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [99] goal: 1231, source line: 162, command: 'rule ifthenelse_split occ=0' 
623167     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [100] goal: 1232, source line: 163, command: 'tryclose branch' 
623210     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [101] goal: 1233, source line: 164, command: 'tryclose branch' 
623215     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [102] goal: 1228, source line: 165, command: 'tryclose branch' 
623298     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]'' 
623307     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [104] goal: 1397, source line: 169, command: 'rule seqNPermInjective' 
623308     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'' 
623310     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'' 
623311     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [107] goal: 1401, source line: 172, command: 'rule impLeft' 
623312     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [108] goal: 1402, source line: 173, command: 'tryclose branch' 
623451     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [109] goal: 1403, source line: 174, command: 'tryclose branch' 
623456     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'' 
623459     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)'' 
623461     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [112] goal: 1536, source line: 179, command: 'rule andRight' 
623462     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [113] goal: 1537, source line: 181, command: 'rule andRight' 
623465     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [114] goal: 1539, source line: 182, command: 'rule andRight' 
623466     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [115] goal: 1541, source line: 183, command: 'rule andRight' 
623468     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [116] goal: 1543, source line: 184, command: 'tryclose branch' 
623477     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [117] goal: 1544, source line: 185, command: 'rule seqNPermSwapNPerm' 
623483     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'' 
623485     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [119] goal: 1559, source line: 188, command: 'instantiate hide var=jv with='jv_1'' 
623486     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [120] goal: 1560, source line: 189, command: 'tryclose branch' 
623580     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [121] goal: 1542, source line: 190, command: 'rule allRight' 
623581     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [122] goal: 1667, source line: 192, command: 'rule impRight' 
623582     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [123] goal: 1668, source line: 193, command: 'rule andLeft' 
623583     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [124] goal: 1669, source line: 194, command: 'instantiate var=iv with='v_iv_0'' 
623584     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [125] goal: 1670, source line: 195, command: 'rule impLeft' 
623585     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [126] goal: 1671, source line: 196, command: 'tryclose branch' 
623685     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [127] goal: 1672, source line: 197, command: 'rule getOfSwap' 
623686     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [128] goal: 1786, source line: 198, command: 'rule ifthenelse_negated' 
623688     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [129] goal: 1787, source line: 199, command: 'rule ifthenelse_split occ=0' 
623689     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [130] goal: 1788, source line: 200, command: 'rule andLeft' 
623690     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [131] goal: 1790, source line: 201, command: 'rule andLeft' 
623691     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [132] goal: 1791, source line: 202, command: 'rule andLeft' 
623691     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [133] goal: 1792, source line: 203, command: 'rule ifthenelse_split occ=0' 
623692     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [134] goal: 1793, source line: 204, command: 'tryclose branch' 
623771     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [135] goal: 1794, source line: 205, command: 'rule ifthenelse_split occ=0' 
623772     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [136] goal: 1885, source line: 206, command: 'tryclose branch' 
623847     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [137] goal: 1886, source line: 207, command: 'instantiate var=iv with='v_y_0'' 
623848     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [138] goal: 1968, source line: 208, command: 'rule impLeft' 
623848     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [139] goal: 1969, source line: 209, command: 'tryclose branch' 
623853     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [140] goal: 1970, source line: 210, command: 'tryclose branch' 
623857     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [141] goal: 1789, source line: 211, command: 'tryclose branch' 
623862     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [142] goal: 1540, source line: 212, command: 'tryclose branch' 
623983     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [143] goal: 1538, source line: 213, command: 'rule getOfSwap' 
623984     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [144] goal: 2097, source line: 215, command: 'rule ifthenelse_negated' 
623985     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [145] goal: 2098, source line: 216, command: 'rule ifthenelse_split occ=0' 
623986     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [146] goal: 2099, source line: 217, command: 'tryclose branch' 
623996     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [147] goal: 2100, source line: 218, command: 'tryclose branch' 
624075     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [148] goal: 1535, source line: 219, command: 'tryclose branch' 
627539     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'' 
627540     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)'' 
627544     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [151] goal: 4268, source line: 226, command: 'rule andRight' 
627546     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [152] goal: 4269, source line: 228, command: 'rule andRight' 
627547     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [153] goal: 4271, source line: 229, command: 'rule andRight' 
627548     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [154] goal: 4273, source line: 230, command: 'rule andRight' 
627548     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [155] goal: 4275, source line: 231, command: 'tryclose branch' 
627556     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [156] goal: 4276, source line: 232, command: 'rule seqNPermSwapNPerm' 
627557     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'' 
627558     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [158] goal: 4288, source line: 235, command: 'instantiate hide var=jv with='jv_0'' 
627559     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [159] goal: 4289, source line: 236, command: 'rule impLeft' 
627560     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [160] goal: 4290, source line: 237, command: 'tryclose branch' 
627652     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [161] goal: 4291, source line: 238, command: 'tryclose branch' 
627657     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [162] goal: 4274, source line: 239, command: 'rule allRight' 
627658     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [163] goal: 4400, source line: 241, command: 'rule impRight' 
627659     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [164] goal: 4401, source line: 242, command: 'rule andLeft' 
627660     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [165] goal: 4402, source line: 243, command: 'instantiate var=iv with='v_iv_0'' 
627660     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [166] goal: 4403, source line: 244, command: 'rule impLeft' 
627661     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [167] goal: 4404, source line: 245, command: 'tryclose branch' 
627752     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [168] goal: 4405, source line: 246, command: 'rule getOfSwap' 
627754     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [169] goal: 4521, source line: 247, command: 'rule ifthenelse_negated' 
627755     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [170] goal: 4522, source line: 248, command: 'rule ifthenelse_split occ=0' 
627758     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [171] goal: 4523, source line: 249, command: 'rule andLeft' 
627759     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [172] goal: 4525, source line: 250, command: 'rule andLeft' 
627759     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [173] goal: 4526, source line: 251, command: 'rule andLeft' 
627760     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [174] goal: 4527, source line: 252, command: 'rule ifthenelse_split occ=0' 
627761     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [175] goal: 4528, source line: 253, command: 'tryclose branch' 
627840     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [176] goal: 4529, source line: 254, command: 'rule ifthenelse_split occ=0' 
627842     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [177] goal: 4622, source line: 255, command: 'tryclose branch' 
627924     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [178] goal: 4623, source line: 256, command: 'tryclose branch' 
627928     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [179] goal: 4524, source line: 257, command: 'tryclose branch' 
627933     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [180] goal: 4272, source line: 258, command: 'rule getOfSwap' 
627934     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [181] goal: 4713, source line: 260, command: 'rule ifthenelse_negated' 
627935     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [182] goal: 4714, source line: 261, command: 'rule ifthenelse_split occ=0' 
627936     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [183] goal: 4715, source line: 262, command: 'tryclose branch' 
627947     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [184] goal: 4716, source line: 263, command: 'tryclose branch' 
628033     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [185] goal: 4270, source line: 264, command: 'rule getOfSwap' 
628034     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [186] goal: 4839, source line: 266, command: 'rule ifthenelse_negated' 
628035     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [187] goal: 4840, source line: 267, command: 'rule ifthenelse_split occ=0' 
628036     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [188] goal: 4841, source line: 268, command: 'tryclose branch' 
628115     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [189] goal: 4842, source line: 269, command: 'tryclose branch' 
628128     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'' 
628129     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)'' 
628130     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [192] goal: 4950, source line: 275, command: 'rule andRight' 
628132     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [193] goal: 4951, source line: 277, command: 'rule andRight' 
628133     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [194] goal: 4953, source line: 278, command: 'rule andRight' 
628133     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [195] goal: 4955, source line: 279, command: 'rule andRight' 
628134     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [196] goal: 4957, source line: 280, command: 'tryclose branch' 
628145     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [197] goal: 4958, source line: 281, command: 'rule seqNPermSwapNPerm' 
628146     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [198] goal: 4977, source line: 283, command: 'instantiate hide var=iv with='jv_0'' 
628147     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'' 
628148     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [200] goal: 4979, source line: 285, command: 'rule impLeft' 
628149     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [201] goal: 4980, source line: 286, command: 'tryclose branch' 
628234     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))'' 
628235     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [203] goal: 5093, source line: 288, command: 'instantiate hide var=iv with='jv_0'' 
628236     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'' 
628237     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [205] goal: 5095, source line: 290, command: 'rule impLeft' 
628238     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [206] goal: 5096, source line: 291, command: 'tryclose branch' 
628326     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [207] goal: 5097, source line: 292, command: 'tryclose branch' 
628331     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [208] goal: 4956, source line: 293, command: 'rule allRight' 
628333     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [209] goal: 5212, source line: 295, command: 'rule impRight' 
628334     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [210] goal: 5213, source line: 296, command: 'rule andLeft' 
628334     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [211] goal: 5214, source line: 297, command: 'instantiate var=iv with='v_iv_0'' 
628335     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [212] goal: 5215, source line: 300, command: 'rule impLeft' 
628336     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [213] goal: 5216, source line: 301, command: 'tryclose branch' 
628473     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [214] goal: 5217, source line: 302, command: 'rule getOfSwap' 
628474     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [215] goal: 5337, source line: 304, command: 'rule ifthenelse_negated' 
628475     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [216] goal: 5338, source line: 305, command: 'rule ifthenelse_split occ=0' 
628476     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [217] goal: 5339, source line: 306, command: 'rule andLeft' 
628477     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [218] goal: 5341, source line: 307, command: 'rule andLeft' 
628478     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [219] goal: 5342, source line: 308, command: 'rule andLeft' 
628478     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [220] goal: 5343, source line: 309, command: 'rule ifthenelse_split occ=0' 
628479     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [221] goal: 5344, source line: 310, command: 'rule getOfSwap' 
628480     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [222] goal: 5346, source line: 311, command: 'rule ifthenelse_negated' 
628481     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [223] goal: 5347, source line: 312, command: 'rule ifthenelse_split occ=0' 
628481     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [224] goal: 5348, source line: 313, command: 'rule andLeft' 
628482     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [225] goal: 5350, source line: 314, command: 'rule andLeft' 
628483     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [226] goal: 5351, source line: 315, command: 'rule andLeft' 
628483     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [227] goal: 5352, source line: 316, command: 'rule ifthenelse_split occ=0' 
628484     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [228] goal: 5353, source line: 317, command: 'tryclose branch' 
628566     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [229] goal: 5354, source line: 318, command: 'rule ifthenelse_split occ=0' 
628567     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [230] goal: 5463, source line: 319, command: 'tryclose branch' 
628573     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [231] goal: 5464, source line: 320, command: 'tryclose branch' 
628645     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [232] goal: 5349, source line: 321, command: 'tryclose branch' 
628720     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [233] goal: 5345, source line: 322, command: 'rule ifthenelse_split' 
628721     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [234] goal: 5660, source line: 324, command: 'rule getOfSwap' 
628722     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [235] goal: 5662, source line: 325, command: 'rule ifthenelse_negated' 
628723     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [236] goal: 5663, source line: 326, command: 'rule ifthenelse_split occ=0' 
628724     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [237] goal: 5664, source line: 327, command: 'rule andLeft' 
628724     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [238] goal: 5666, source line: 328, command: 'rule andLeft' 
628725     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [239] goal: 5667, source line: 329, command: 'rule andLeft' 
628725     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [240] goal: 5668, source line: 330, command: 'rule ifthenelse_split occ=0' 
628725     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [241] goal: 5669, source line: 331, command: 'tryclose branch' 
628806     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [242] goal: 5670, source line: 332, command: 'tryclose branch' 
628812     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [243] goal: 5665, source line: 333, command: 'tryclose branch' 
628896     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [244] goal: 5661, source line: 334, command: 'rule getOfSwap' 
628897     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [245] goal: 5887, source line: 336, command: 'rule ifthenelse_negated' 
628898     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [246] goal: 5888, source line: 337, command: 'rule ifthenelse_split occ=0' 
628899     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [247] goal: 5889, source line: 338, command: 'rule andLeft' 
628899     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [248] goal: 5891, source line: 339, command: 'rule andLeft' 
628900     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [249] goal: 5892, source line: 340, command: 'rule andLeft' 
628900     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [250] goal: 5893, source line: 341, command: 'rule ifthenelse_split occ=0' 
628900     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [251] goal: 5894, source line: 342, command: 'tryclose branch' 
628905     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [252] goal: 5895, source line: 343, command: 'rule ifthenelse_split occ=0' 
628906     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [253] goal: 5897, source line: 344, command: 'tryclose branch' 
628981     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [254] goal: 5898, source line: 345, command: 'tryclose branch' 
628986     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [255] goal: 5890, source line: 346, command: 'tryclose branch' 
628991     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [256] goal: 5340, source line: 347, command: 'tryclose branch' 
629084     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [257] goal: 4954, source line: 348, command: 'rule getOfSwap' 
629085     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [258] goal: 6115, source line: 350, command: 'rule ifthenelse_negated' 
629086     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [259] goal: 6116, source line: 351, command: 'rule ifthenelse_split occ=0' 
629087     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [260] goal: 6117, source line: 352, command: 'rule andLeft' 
629087     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [261] goal: 6119, source line: 353, command: 'rule andLeft' 
629087     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [262] goal: 6120, source line: 354, command: 'rule andLeft' 
629088     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [263] goal: 6121, source line: 355, command: 'rule ifthenelse_split occ=0' 
629088     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [264] goal: 6122, source line: 356, command: 'tryclose branch' 
629140     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [265] goal: 6123, source line: 357, command: 'rule ifthenelse_split occ=0' 
629141     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [266] goal: 6193, source line: 358, command: 'rule getOfSwap' 
629141     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [267] goal: 6195, source line: 359, command: 'rule ifthenelse_negated' 
629142     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [268] goal: 6196, source line: 360, command: 'rule ifthenelse_split occ=0' 
629143     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [269] goal: 6197, source line: 361, command: 'tryclose branch' 
629148     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [270] goal: 6198, source line: 362, command: 'tryclose branch' 
629154     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [271] goal: 6194, source line: 363, command: 'tryclose branch' 
629264     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [272] goal: 6118, source line: 364, command: 'tryclose branch' 
629347     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [273] goal: 4952, source line: 365, command: 'rule getOfSwap' 
629348     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [274] goal: 6456, source line: 367, command: 'rule ifthenelse_negated' 
629349     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [275] goal: 6457, source line: 368, command: 'rule ifthenelse_split occ=0' 
629350     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [276] goal: 6458, source line: 369, command: 'tryclose branch' 
629521     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [277] goal: 6459, source line: 370, command: 'tryclose branch' 
629606     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'' 
629606     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [279] goal: 6735, source line: 375, command: 'tryclose branch' 
632586     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [280] goal: 6735, source line: 378, command: 'rule seqNPermSwapNPerm' 
632591     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [281] goal: 8783, source line: 380, command: 'instantiate hide var=iv with='jv_1'' 
632592     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'' 
632593     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [283] goal: 8785, source line: 382, command: 'rule impLeft' 
632594     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [284] goal: 8786, source line: 383, command: 'tryclose branch' 
632711     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))'' 
632712     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [286] goal: 8909, source line: 385, command: 'instantiate hide var=iv with='jv_1'' 
632713     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'' 
632714     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [288] goal: 8911, source line: 387, command: 'rule impLeft' 
632715     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [289] goal: 8912, source line: 388, command: 'tryclose branch' 
632816     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [290] goal: 8913, source line: 389, command: 'tryclose branch' 
635702     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [291] goal: 6736, source line: 390, command: 'tryclose branch' 
638790     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [292] goal: 6736, source line: 397, command: 'rule seqNPermSwapNPerm formula='seqNPerm(s_0)'' 
638794     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'' 
638795     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [294] goal: 12634, source line: 400, command: 'instantiate hide var=jv with='jv_0'' 
638796     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [295] goal: 12635, source line: 401, command: 'rule impLeft' 
638797     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [296] goal: 12636, source line: 402, command: 'tryclose branch' 
638906     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))'' 
638907     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'' 
638908     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [299] goal: 12758, source line: 405, command: 'instantiate hide var=jv with='jv_1'' 
638909     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)' ...' 
638910     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [301] goal: 12760, source line: 407, command: 'tryclose branch' 
640045     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm2/Taclet_schiffl_thm_1.proof 
640045     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 90.6ns 
640046     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
642480     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.43s 
642480     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: schiffl_thm_1 
643348     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: schiffl_thm_1 
643350     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 8.1ns 
643350     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [1] goal: 0, source line: 50, command: 'macro split-prop' 
643359     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)'' 
643368     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [3] goal: 11, source line: 52, command: 'instantiate hide var=x with='f_x'' 
643371     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [4] goal: 12, source line: 53, command: 'instantiate hide var=y with='f_y'' 
643373     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [5] goal: 13, source line: 54, command: 'rule impLeft' 
643374     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [6] goal: 14, source line: 55, command: 'tryclose branch' 
643379     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [7] goal: 15, source line: 56, command: 'rule exLeft' 
643380     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [8] goal: 23, source line: 57, command: 'macro split-prop' 
643385     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [9] goal: 27, source line: 58, command: 'rule seqPermDef occ=1' 
643385     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [10] goal: 28, source line: 59, command: 'rule andRight' 
643388     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [11] goal: 29, source line: 60, command: 'tryclose branch' 
643397     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [12] goal: 30, source line: 61, command: 'instantiate hide var=s with='r_0'' 
643397     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [13] goal: 46, source line: 62, command: 'rule andRight' 
643399     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [14] goal: 47, source line: 63, command: 'tryclose branch' 
643444     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [15] goal: 48, source line: 64, command: 'rule allRight' 
643444     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [16] goal: 119, source line: 65, command: 'rule impRight' 
643445     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [17] goal: 120, source line: 66, command: 'instantiate hide var=iv with='iv_0'' 
643445     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [18] goal: 121, source line: 67, command: 'rule impLeft' 
643446     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [19] goal: 122, source line: 68, command: 'tryclose branch' 
643503     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [20] goal: 123, source line: 69, command: 'rule andLeft' 
643504     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [21] goal: 203, source line: 70, command: 'rule seqNPermRange' 
643504     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [22] goal: 204, source line: 71, command: 'instantiate hide var=iv with='iv_0'' 
643505     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [23] goal: 205, source line: 72, command: 'rule impLeft' 
643506     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [24] goal: 206, source line: 73, command: 'tryclose branch' 
643509     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [25] goal: 207, source line: 74, command: 'rule andLeft' 
643509     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [26] goal: 215, source line: 75, command: 'rule andLeft' 
643510     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [27] goal: 216, source line: 76, command: 'rule seqNPermRange' 
643510     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [28] goal: 217, source line: 77, command: 'instantiate hide var=iv with='f_x'' 
643511     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [29] goal: 218, source line: 78, command: 'rule impLeft' 
643512     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [30] goal: 219, source line: 79, command: 'tryclose branch' 
643581     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [31] goal: 220, source line: 80, command: 'rule andLeft' 
643582     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [32] goal: 311, source line: 81, command: 'rule andLeft' 
643582     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [33] goal: 312, source line: 82, command: 'rule seqNPermRange' 
643582     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [34] goal: 313, source line: 83, command: 'instantiate hide var=iv with='f_y'' 
643583     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [35] goal: 314, source line: 84, command: 'rule impLeft' 
643584     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [36] goal: 315, source line: 85, command: 'tryclose branch' 
643650     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [37] goal: 316, source line: 86, command: 'rule andLeft' 
643650     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [38] goal: 410, source line: 87, command: 'rule andLeft' 
643651     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [39] goal: 411, source line: 88, command: 'rule getOfSeqDef occ=0' 
643651     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [40] goal: 412, source line: 89, command: 'rule getOfSeqDef' 
643652     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [41] goal: 413, source line: 90, command: 'rule ifthenelse_split occ=0' 
643652     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [42] goal: 414, source line: 91, command: 'rule andLeft occ=0' 
643653     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [43] goal: 416, source line: 92, command: 'rule sub_zero_2 occ=0' 
643653     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [44] goal: 417, source line: 93, command: 'rule ifthenelse_split occ=2' 
643654     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [45] goal: 418, source line: 94, command: 'rule andLeft' 
643654     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [46] goal: 420, source line: 95, command: 'rule sub_zero_2 occ=0' 
643654     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [47] goal: 421, source line: 96, command: 'rule add_zero_right occ=0' 
643655     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [48] goal: 422, source line: 97, command: 'rule add_zero_right occ=0' 
643655     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [49] goal: 423, source line: 98, command: 'rule add_zero_right occ=0' 
643655     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [50] goal: 424, source line: 99, command: 'rule add_zero_right occ=0' 
643656     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [51] goal: 425, source line: 100, command: 'rule add_zero_right occ=0' 
643656     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [52] goal: 426, source line: 101, command: 'rule add_zero_right occ=0' 
643656     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [53] goal: 427, source line: 102, command: 'rule ifthenelse_split occ=0' 
643657     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [54] goal: 428, source line: 103, command: 'rule ifthenelse_split occ=0' 
643657     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [55] goal: 430, source line: 104, command: 'tryclose branch' 
643660     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [56] goal: 431, source line: 105, command: 'tryclose branch' 
643687     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [57] goal: 429, source line: 106, command: 'rule ifthenelse_split occ=0' 
643688     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [58] goal: 473, source line: 107, command: 'tryclose branch' 
643729     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [59] goal: 474, source line: 108, command: 'rule ifthenelse_split occ=0' 
643730     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [60] goal: 541, source line: 109, command: 'rule seqNPermInjective' 
643731     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [61] goal: 543, source line: 110, command: 'instantiate hide var=iv with='iv_0'' 
643732     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [62] goal: 544, source line: 111, command: 'instantiate hide var=jv with='f_y'' 
643733     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [63] goal: 545, source line: 112, command: 'rule impLeft' 
643733     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [64] goal: 546, source line: 113, command: 'tryclose branch' 
643771     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [65] goal: 547, source line: 114, command: 'tryclose branch' 
643773     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [66] goal: 542, source line: 115, command: 'rule ifthenelse_split occ=0' 
643774     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [67] goal: 606, source line: 116, command: 'rule seqNPermInjective' 
643775     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [68] goal: 608, source line: 117, command: 'instantiate hide var=iv with='iv_0'' 
643776     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [69] goal: 609, source line: 118, command: 'instantiate hide var=jv with='f_x'' 
643777     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [70] goal: 610, source line: 119, command: 'rule impLeft' 
643777     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [71] goal: 611, source line: 120, command: 'tryclose branch' 
643817     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [72] goal: 612, source line: 121, command: 'tryclose branch' 
643819     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [73] goal: 607, source line: 122, command: 'tryclose branch' 
643822     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [74] goal: 419, source line: 123, command: 'tryclose branch' 
643869     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [75] goal: 415, source line: 124, command: 'tryclose branch' 
643919     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_eqSameSeq.proof 
643919     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 74ns 
643919     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
646396     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.48s 
646396     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: eqSameSeq 
647218     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: eqSameSeq 
647234     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 12.77ms