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

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

tests
0

failures
0

ignored
13m34.71s

duration
100%

successful

Tests

Test Method name Duration Result
powPositive data()[100] 3.877s passed
powPositiveConcrete data()[101] 3.908s passed
powGeq1Concrete data()[102] 3.821s passed
pow2InIntLower data()[103] 3.765s passed
pow2InIntUpper data()[104] 3.911s passed
logSelfConcrete data()[105] 3.969s passed
log1Concrete data()[106] 3.917s passed
logProduct data()[107] 3.888s passed
logTimesBaseConcrete data()[108] 3.927s passed
logProdIdentity data()[109] 3.891s passed
moduloByteIsInByte data()[10] 4.134s passed
logProdIdentityConcrete data()[110] 3.851s passed
logPowIdentity data()[111] 3.848s passed
logPowIdentityConcrete data()[112] 4.007s passed
logPositive data()[113] 4.026s passed
logPositiveConcrete data()[114] 4.021s passed
logMono data()[115] 3.939s passed
logMonoConcrete data()[116] 3.997s passed
powLogLess data()[117] 3.977s passed
powLogMore2 data()[118] 3.999s passed
logLessThanPow data()[119] 3.973s passed
moduloCharIsInChar data()[11] 4.128s passed
logLessThanPowConcrete data()[120] 3.968s passed
logSqueeze data()[121] 3.904s passed
ifthenelse_equals data()[122] 4.060s passed
ifthenelse_equals_1 data()[123] 3.917s passed
ifthenelse_equals_2 data()[124] 4.059s passed
disjointWithSingleton1 data()[125] 3.970s passed
disjointWithSingleton2 data()[126] 3.952s passed
disjointArrayRanges data()[127] 3.968s passed
disjointArrayRangeAllFields1 data()[128] 4.088s passed
disjointArrayRangeAllFields2 data()[129] 4.025s passed
div_unique1 data()[12] 4.056s passed
seqSelfDefinition data()[130] 4.032s passed
seqOutsideValue data()[131] 3.967s passed
castedGetAny data()[132] 3.848s passed
seqGetAlphaCast data()[133] 4.039s passed
getOfSeqSingleton data()[134] 3.951s passed
getOfSeqSingletonConcrete data()[135] 3.951s passed
getOfSeqConcat data()[136] 3.933s passed
getOfSeqSub data()[137] 3.867s passed
getOfSeqReverse data()[138] 3.901s passed
lenOfSeqEmpty data()[139] 3.997s passed
div_unique2 data()[13] 4.114s passed
lenOfSeqSingleton data()[140] 3.837s passed
lenOfSeqConcat data()[141] 3.841s passed
lenOfSeqSub data()[142] 3.943s passed
lenOfSeqReverse data()[143] 3.966s passed
equalityToSeqGetAndSeqLenLeft data()[144] 4.008s passed
equalityToSeqGetAndSeqLenRight data()[145] 3.933s passed
getOfSeqSingletonEQ data()[146] 3.982s passed
getOfSeqConcatEQ data()[147] 4.029s passed
getOfSeqSubEQ data()[148] 3.936s passed
getOfSeqReverseEQ data()[149] 4.036s passed
div_exists data()[14] 4.225s passed
lenOfSeqEmptyEQ data()[150] 3.967s passed
lenOfSeqSingletonEQ data()[151] 4.018s passed
lenOfSeqConcatEQ data()[152] 4.037s passed
lenOfSeqSubEQ data()[153] 4.004s passed
lenOfSeqReverseEQ data()[154] 4.083s passed
getOfSeqDefEQ data()[155] 3.959s passed
lenOfSeqDefEQ data()[156] 3.949s passed
seqConcatWithSeqEmpty1 data()[157] 3.914s passed
seqConcatWithSeqEmpty2 data()[158] 4.009s passed
seqReverseOfSeqEmpty data()[159] 3.958s passed
div_one data()[15] 4.094s passed
subSeqComplete data()[160] 4.041s passed
subSeqTailR data()[161] 4.073s passed
subSeqTailL data()[162] 4.023s passed
subSeqTailEQR data()[163] 4.086s passed
subSeqTailEQL data()[164] 3.894s passed
seqDef_split data()[165] 3.993s passed
seqDef_induction_upper data()[166] 3.988s passed
seqDef_induction_upper_concrete data()[167] 4.035s passed
seqDef_induction_lower data()[168] 3.874s passed
seqDef_induction_lower_concrete data()[169] 3.931s passed
jdiv_one data()[16] 4.034s passed
seqDef_split_in_three data()[170] 3.920s passed
seqDef_empty data()[171] 3.870s passed
seqDef_one_summand data()[172] 3.920s passed
seqDef_lower_equals_upper data()[173] 4.002s passed
seqDefOfSeq data()[174] 3.924s passed
seqSelfDefinitionEQ2 data()[175] 3.931s passed
indexOfSeqSingleton data()[176] 3.866s passed
indexOfSeqConcatFirst data()[177] 3.947s passed
indexOfSeqConcatSecond data()[178] 3.970s passed
indexOfSeqSub data()[179] 4.058s passed
div_zero data()[17] 4.117s passed
lenOfArray2seq data()[180] 4.042s passed
getAnyOfArray2seq data()[181] 4.001s passed
getOfArray2seq data()[182] 4.037s passed
getAnyOfNPermInv data()[183] 3.906s passed
seqNPermRange data()[184] 4.134s passed
seqPermTrans data()[185] 3.984s passed
seqPermRefl data()[186] 3.962s passed
seqPermSplit data()[187] 4.018s passed
seqNPermRight data()[188] 4.216s passed
seqPermFromSwap data()[189] 4.029s passed
divResZero1 data()[18] 4.099s passed
seqPermTransAlt0 data()[190] 4.063s passed
seqPermTransAlt1 data()[191] 4.011s passed
seqPermTransAlt2 data()[192] 4.001s passed
seqPermTransAlt3 data()[193] 3.891s passed
seqPermForall data()[194] 4.061s passed
seqPermExists data()[195] 4.042s passed
schiffl_lemma_2 data()[196] 26.453s passed
schiffl_thm_1 data()[197] 4.797s passed
eqSameSeq data()[198] 3.940s passed
divResZero2 data()[19] 4.062s passed
eqTermCut data()[1] 4.845s passed
divResOne1 data()[20] 4.033s passed
divResOne2 data()[21] 3.919s passed
div_cancel1 data()[22] 4.032s passed
div_cancel2 data()[23] 3.971s passed
divAddMultDenom data()[24] 4.095s passed
divMinus data()[25] 4.032s passed
divMinusDenom data()[26] 4.147s passed
divLeastDPos data()[27] 3.976s passed
divLeastDNeg data()[28] 3.928s passed
divGreatestDPos data()[29] 3.929s passed
equivAllRight data()[2] 4.441s passed
divGreatestDNeg data()[30] 3.990s passed
divIncreasingPos data()[31] 4.041s passed
divIncreasingNeg data()[32] 3.882s passed
jdiv_zero data()[33] 3.963s passed
jdivPulloutMinusNum data()[34] 3.905s passed
jdivPulloutMinusDenom data()[35] 3.911s passed
jdiv_uniquePosPos data()[36] 3.954s passed
jdiv_uniquePosNeg data()[37] 4.095s passed
jdiv_uniqueNegPos data()[38] 4.011s passed
jdiv_uniqueNegNeg data()[39] 3.950s passed
irrflConcrete1 data()[3] 4.373s passed
jdivMultDenom1 data()[40] 3.992s passed
jdivMultDenom2 data()[41] 3.947s passed
mod_geZero data()[42] 3.867s passed
mod_lessDenom data()[43] 3.981s passed
jmod_NumPos data()[44] 4.016s passed
jmod_NumNeg data()[45] 4.050s passed
jmod_geZero data()[46] 4.039s passed
jmodNumZero data()[47] 3.907s passed
jmod_pulloutminusNum data()[48] 4.034s passed
jmod_pulloutminusDenom data()[49] 3.941s passed
irrflConcrete2 data()[4] 4.203s passed
jmodUnique1 data()[50] 4.093s passed
jmodUnique2 data()[51] 4.030s passed
intDivRem data()[52] 4.010s passed
jmodjmod data()[53] 4.005s passed
jmodDivisible data()[54] 4.132s passed
jmodDivisibleRep data()[55] 4.020s passed
jdivAddMultDenom data()[56] 4.213s passed
jmodAltZero data()[57] 3.914s passed
jmodAddMultDenomZero data()[58] 3.982s passed
polyDiv_zero data()[59] 3.971s passed
cancel_gtPos data()[5] 4.075s passed
polyMod_ltdivDenom data()[60] 4.041s passed
bsum_empty data()[61] 3.965s passed
bsum_induction_upper data()[62] 3.902s passed
bsum_induction_lower data()[63] 3.912s passed
bsum_num_of_bounds data()[64] 3.912s passed
bsum_num_of_bounds2 data()[65] 3.890s passed
bsum_induction_upper2 data()[66] 3.906s passed
bsum_induction_upper_concrete data()[67] 4.092s passed
bsum_induction_upper_concrete_2 data()[68] 4.045s passed
bsum_induction_upper2_concrete data()[69] 3.989s passed
cancel_gtNeg data()[6] 4.087s passed
bsum_induction_lower_concrete data()[70] 3.987s passed
bsum_induction_lower2 data()[71] 3.984s passed
bsum_induction_lower2_concrete data()[72] 3.918s passed
bsum_positive data()[73] 3.997s passed
bsum_upper_bound data()[74] 3.953s passed
bsum_lower_bound data()[75] 3.993s passed
bsum_positive_lower_bound_element data()[76] 4.029s passed
bsum_sub_same_index data()[77] 3.859s passed
bsum_less_same_index data()[78] 4.053s passed
bsum_equal_except_one_index data()[79] 4.008s passed
moduloIntIsInInt data()[7] 3.955s passed
bsum_num_of_is_max data()[80] 4.098s passed
bsum_num_of_is_max2 data()[81] 3.993s passed
bsum_num_of_is_max3 data()[82] 4.056s passed
bsum_num_of_is_max4 data()[83] 4.121s passed
bsum_num_of_lt_max data()[84] 3.989s passed
bsum_num_of_lt_max2 data()[85] 4.081s passed
bsum_num_of_lt_max3 data()[86] 4.109s passed
bsum_num_of_lt_max4 data()[87] 3.979s passed
bsum_num_of_gt0 data()[88] 4.079s passed
bsum_num_of_gt0_alt data()[89] 3.999s passed
moduloLongIsInLong data()[8] 4.045s passed
bsum_add_concrete data()[90] 3.962s passed
bprod_all_positive data()[91] 3.998s passed
bprod_split data()[92] 3.913s passed
powConcrete0 data()[93] 3.960s passed
powConcrete1 data()[94] 3.985s passed
powSplitFactor data()[95] 3.961s passed
powAdd data()[96] 3.905s passed
powMono data()[97] 3.920s passed
powMonoConcrete data()[98] 3.909s passed
powMonoConcreteRight data()[99] 3.926s passed
moduloShortIsInShort data()[9] 4.087s passed

Standard output

436        INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src/test/resources/testcase/dummyTrue.key 
470        DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 13.95ms 
780        INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
805        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)

2017       DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for Meta 
2024       DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for Meta 
2027       DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for Meta 
2029       DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for Meta 
3694       DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for JavaBigintExpression 
10504      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 9.72s 
10607      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof dummyTrue.key 
10656      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 32.7ns 
10675      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/firstOrder/Taclet_eqTermCut.proof 
10675      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 169.2ns 
10684      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
14290      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.61s 
14293      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: eqTermCut 
15479      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: eqTermCut 
15509      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 23.7ms 
15520      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/firstOrder/Taclet_equivAllRight.proof 
15520      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 168.2ns 
15522      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
18914      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.39s 
18915      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: equivAllRight 
19927      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: equivAllRight 
19957      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 18.48ms 
19963      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_irrflConcrete1.proof 
19963      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 530.8ns 
19969      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
23230      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.26s 
23230      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: irrflConcrete1 
24327      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: irrflConcrete1 
24334      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.28ms 
24338      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_irrflConcrete2.proof 
24338      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 464.6ns 
24340      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
27513      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.17s 
27515      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: irrflConcrete2 
28533      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: irrflConcrete2 
28538      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.92ms 
28541      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_cancel_gtPos.proof 
28541      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 154.6ns 
28543      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
31565      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.02s 
31566      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: cancel_gtPos 
32565      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: cancel_gtPos 
32613      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 44.22ms 
32617      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_cancel_gtNeg.proof 
32617      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 387.6ns 
32619      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
35757      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.14s 
35758      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: cancel_gtNeg 
36676      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: cancel_gtNeg 
36700      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 19.66ms 
36704      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intRulesIgnoringOF/Taclet_moduloIntIsInInt.proof 
36704      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 396.5ns 
36706      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
39753      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.05s 
39754      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: moduloIntIsInInt 
40654      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: moduloIntIsInInt 
40657      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 834.8ns 
40659      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intRulesIgnoringOF/Taclet_moduloLongIsInLong.proof 
40659      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 101ns 
40660      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
43766      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.11s 
43766      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: moduloLongIsInLong 
44699      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: moduloLongIsInLong 
44702      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 625.8ns 
44705      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intRulesIgnoringOF/Taclet_moduloShortIsInShort.proof 
44705      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 354.6ns 
44706      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
47770      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.06s 
47771      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: moduloShortIsInShort 
48786      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: moduloShortIsInShort 
48789      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 728.8ns 
48791      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intRulesIgnoringOF/Taclet_moduloByteIsInByte.proof 
48791      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 117.3ns 
48792      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
51918      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.13s 
51919      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: moduloByteIsInByte 
52920      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: moduloByteIsInByte 
52923      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 652.2ns 
52926      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intRulesIgnoringOF/Taclet_moduloCharIsInChar.proof 
52926      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 512.1ns 
52927      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
56013      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.09s 
56013      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: moduloCharIsInChar 
57047      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: moduloCharIsInChar 
57050      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 735.6ns 
57054      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_div_unique1.proof 
57054      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 435.7ns 
57055      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
60060      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3s 
60061      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: div_unique1 
61058      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: div_unique1 
61107      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 44.72ms 
61127      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_div_unique2.proof 
61129      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 2.31ms 
61131      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
64197      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.07s 
64197      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: div_unique2 
65184      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: div_unique2 
65228      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 39.9ms 
65231      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_div_exists.proof 
65232      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 802.1ns 
65234      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
68278      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.04s 
68279      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: div_exists 
69258      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: div_exists 
69452      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 185.01ms 
69456      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_div_one.proof 
69457      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 412.4ns 
69458      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
72570      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.11s 
72571      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: div_one 
73543      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: div_one 
73549      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.26ms 
73550      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdiv_one.proof 
73550      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 109ns 
73551      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
76594      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.04s 
76594      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdiv_one 
77577      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdiv_one 
77582      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.42ms 
77584      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_div_zero.proof 
77585      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 121.7ns 
77586      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
80631      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.04s 
80632      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: div_zero 
81645      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: div_zero 
81699      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 48.67ms 
81702      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divResZero1.proof 
81703      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 371.7ns 
81704      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
84768      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.06s 
84769      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divResZero1 
85781      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divResZero1 
85798      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 12.67ms 
85801      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divResZero2.proof 
85801      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 393.8ns 
85803      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
88859      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.06s 
88860      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divResZero2 
89844      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divResZero2 
89860      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 12.91ms 
89861      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divResOne1.proof 
89861      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 108.4ns 
89863      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
92868      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.01s 
92869      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divResOne1 
93874      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divResOne1 
93893      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 15.15ms 
93895      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divResOne2.proof 
93896      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 359.1ns 
93897      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
96812      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.92s 
96813      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divResOne2 
97796      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divResOne2 
97813      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 13.4ms 
97815      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_div_cancel1.proof 
97815      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 360.6ns 
97816      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
100853     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.04s 
100853     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: div_cancel1 
101818     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: div_cancel1 
101844     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 20.98ms 
101846     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_div_cancel2.proof 
101847     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 393.8ns 
101848     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
104854     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.01s 
104855     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: div_cancel2 
105812     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: div_cancel2 
105815     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.66ms 
105817     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divAddMultDenom.proof 
105817     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 94.4ns 
105818     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
108849     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.03s 
108850     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divAddMultDenom 
109862     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divAddMultDenom 
109910     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 40.94ms 
109913     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divMinus.proof 
109913     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 425.7ns 
109915     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
112922     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.01s 
112923     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divMinus 
113875     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divMinus 
113941     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 58.27ms 
113944     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divMinusDenom.proof 
113945     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 341.7ns 
113946     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
117096     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.15s 
117096     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divMinusDenom 
118040     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divMinusDenom 
118088     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 40.94ms 
118091     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divLeastDPos.proof 
118091     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 125.3ns 
118092     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
121098     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.01s 
121100     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divLeastDPos 
122055     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divLeastDPos 
122064     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 6.75ms 
122069     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divLeastDNeg.proof 
122070     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 754.49ns 
122071     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
125027     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.96s 
125027     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divLeastDNeg 
125977     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divLeastDNeg 
125994     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 14.6ms 
125996     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divGreatestDPos.proof 
125996     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 103ns 
125997     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
128919     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.92s 
128919     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divGreatestDPos 
129909     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divGreatestDPos 
129923     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 11.81ms 
129925     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divGreatestDNeg.proof 
129925     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 85.9ns 
129926     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
132883     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.96s 
132883     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divGreatestDNeg 
133892     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divGreatestDNeg 
133912     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 14.42ms 
133919     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divIncreasingPos.proof 
133922     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 2.96ms 
133924     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
136938     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.01s 
136938     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divIncreasingPos 
137947     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divIncreasingPos 
137956     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 6.93ms 
137958     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divIncreasingNeg.proof 
137958     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 106.9ns 
137959     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
140922     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.96s 
140922     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divIncreasingNeg 
141829     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divIncreasingNeg 
141838     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 6.98ms 
141840     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdiv_zero.proof 
141840     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 104.8ns 
141841     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
144914     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.07s 
144914     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdiv_zero 
145798     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdiv_zero 
145802     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.75ms 
145803     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdivPulloutMinusNum.proof 
145803     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 79.5ns 
145804     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
148742     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.94s 
148743     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdivPulloutMinusNum 
149694     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdivPulloutMinusNum 
149706     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 9.25ms 
149708     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdivPulloutMinusDenom.proof 
149709     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 363.9ns 
149710     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
152577     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.87s 
152578     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdivPulloutMinusDenom 
153565     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdivPulloutMinusDenom 
153616     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 45.23ms 
153619     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdiv_uniquePosPos.proof 
153619     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 305.7ns 
153621     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
156537     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.92s 
156538     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdiv_uniquePosPos 
157548     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdiv_uniquePosPos 
157571     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 18.21ms 
157573     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdiv_uniquePosNeg.proof 
157574     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 335.2ns 
157575     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
160632     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.06s 
160632     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdiv_uniquePosNeg 
161642     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdiv_uniquePosNeg 
161667     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 19.36ms 
161668     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdiv_uniqueNegPos.proof 
161668     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 101.4ns 
161669     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
164675     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.01s 
164675     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdiv_uniqueNegPos 
165649     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdiv_uniqueNegPos 
165676     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 20.43ms 
165679     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdiv_uniqueNegNeg.proof 
165679     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 588.6ns 
165680     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
168696     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.02s 
168697     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdiv_uniqueNegNeg 
169604     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdiv_uniqueNegNeg 
169627     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 19.78ms 
169629     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdivMultDenom1.proof 
169629     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 84ns 
169630     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
172606     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.98s 
172606     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdivMultDenom1 
173567     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdivMultDenom1 
173619     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 45.06ms 
173626     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdivMultDenom2.proof 
173626     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 426ns 
173627     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
176619     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.99s 
176619     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdivMultDenom2 
177567     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdivMultDenom2 
177571     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.37ms 
177572     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_mod_geZero.proof 
177572     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 96.7ns 
177573     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
180458     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.88s 
180458     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: mod_geZero 
181433     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: mod_geZero 
181438     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.94ms 
181439     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_mod_lessDenom.proof 
181439     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 108.9ns 
181440     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
184474     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.03s 
184474     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: mod_lessDenom 
185408     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: mod_lessDenom 
185418     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 7.34ms 
185420     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmod_NumPos.proof 
185420     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 101.7ns 
185421     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
188486     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.07s 
188486     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmod_NumPos 
189424     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmod_NumPos 
189435     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 8.36ms 
189436     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmod_NumNeg.proof 
189436     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 99.3ns 
189437     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
192500     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.06s 
192500     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmod_NumNeg 
193460     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmod_NumNeg 
193484     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 19.97ms 
193486     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmod_geZero.proof 
193487     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 319.1ns 
193488     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
196492     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3s 
196493     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmod_geZero 
197511     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmod_geZero 
197523     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 8.89ms 
197525     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmodNumZero.proof 
197525     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 112.2ns 
197526     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
200457     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.93s 
200458     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmodNumZero 
201427     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmodNumZero 
201430     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.71ms 
201433     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmod_pulloutminusNum.proof 
201433     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 310.3ns 
201434     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
204471     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.04s 
204471     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmod_pulloutminusNum 
205459     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmod_pulloutminusNum 
205464     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.16ms 
205465     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmod_pulloutminusDenom.proof 
205466     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 127.9ns 
205466     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
208474     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.01s 
208475     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmod_pulloutminusDenom 
209401     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmod_pulloutminusDenom 
209405     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.5ms 
209407     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmodUnique1.proof 
209407     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 110ns 
209408     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
212407     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3s 
212407     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmodUnique1 
213384     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmodUnique1 
213497     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 97.82ms 
213501     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmodUnique2.proof 
213501     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 330.8ns 
213503     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
216452     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.95s 
216452     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmodUnique2 
217413     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmodUnique2 
217528     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 105.74ms 
217532     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_intDivRem.proof 
217532     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 356.1ns 
217533     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
220562     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.03s 
220562     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: intDivRem 
221536     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: intDivRem 
221540     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.74ms 
221541     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmodjmod.proof 
221541     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 166.6ns 
221542     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
224529     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.99s 
224530     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmodjmod 
225503     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmodjmod 
225544     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 37.41ms 
225546     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmodDivisible.proof 
225546     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 267.3ns 
225547     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
228629     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.08s 
228629     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmodDivisible 
229643     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmodDivisible 
229676     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 29.1ms 
229679     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmodDivisibleRep.proof 
229679     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 291ns 
229680     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
232687     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.01s 
232688     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmodDivisibleRep 
233693     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmodDivisibleRep 
233697     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.2ms 
233699     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdivAddMultDenom.proof 
233699     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 307.6ns 
233701     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
236769     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.07s 
236769     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdivAddMultDenom 
237744     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdivAddMultDenom 
237908     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 152.32ms 
237912     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmodAltZero.proof 
237912     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 356.8ns 
237913     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
240914     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3s 
240915     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmodAltZero 
241814     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmodAltZero 
241824     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 8.32ms 
241825     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmodAddMultDenomZero.proof 
241825     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 100.4ns 
241826     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
244833     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.01s 
244833     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmodAddMultDenomZero 
245798     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmodAddMultDenomZero 
245806     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 5.77ms 
245807     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_polyDiv_zero.proof 
245807     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 79.4ns 
245808     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
248748     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.94s 
248748     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: polyDiv_zero 
249756     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: polyDiv_zero 
249776     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 17.28ms 
249778     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_polyMod_ltdivDenom.proof 
249778     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 92.3ns 
249779     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
252843     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.06s 
252843     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: polyMod_ltdivDenom 
253799     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: polyMod_ltdivDenom 
253815     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 8ms 
253819     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_empty.proof 
253819     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 280.5ns 
253821     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
256812     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.99s 
256813     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_empty 
257779     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_empty 
257783     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.75ms 
257784     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_induction_upper.proof 
257785     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 69.3ns 
257785     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
260692     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.91s 
260692     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_upper 
261680     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_induction_upper 
261685     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.86ms 
261686     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_induction_lower.proof 
261686     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 109.9ns 
261687     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
264584     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.9s 
264584     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_lower 
265576     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_induction_lower 
265597     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 17.34ms 
265598     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_bounds.proof 
265599     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 64ns 
265599     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
268523     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.92s 
268524     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_bounds 
269492     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_bounds 
269509     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 14.28ms 
269511     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_bounds2.proof 
269511     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 89.2ns 
269512     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
272457     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.95s 
272458     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_bounds2 
273381     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_bounds2 
273399     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 14.85ms 
273401     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_induction_upper2.proof 
273401     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 276.5ns 
273402     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
276375     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.97s 
276375     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_upper2 
277302     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_induction_upper2 
277306     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.64ms 
277307     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_induction_upper_concrete.proof 
277307     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 76ns 
277308     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
280412     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.1s 
280413     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_upper_concrete 
281394     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_induction_upper_concrete 
281398     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.01ms 
281399     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_induction_upper_concrete_2.proof 
281399     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 86.7ns 
281400     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
284437     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.04s 
284438     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_upper_concrete_2 
285435     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_induction_upper_concrete_2 
285442     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.69ms 
285443     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_induction_upper2_concrete.proof 
285443     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 74.8ns 
285444     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
288429     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.98s 
288429     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_upper2_concrete 
289428     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_induction_upper2_concrete 
289431     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.34ms 
289433     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_induction_lower_concrete.proof 
289433     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 123.7ns 
289434     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
292422     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.99s 
292422     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_lower_concrete 
293416     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_induction_lower_concrete 
293418     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 638.1ns 
293420     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_induction_lower2.proof 
293420     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 75.3ns 
293421     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
296435     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.01s 
296435     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_lower2 
297397     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_induction_lower2 
297402     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.76ms 
297403     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_induction_lower2_concrete.proof 
297404     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 99.5ns 
297404     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
300406     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3s 
300406     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_lower2_concrete 
301317     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_induction_lower2_concrete 
301320     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.02ms 
301321     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_positive.proof 
301321     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 78.6ns 
301322     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
304298     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.98s 
304299     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_positive 
305272     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_positive 
305317     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 41.1ms 
305319     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_upper_bound.proof 
305319     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 276.7ns 
305321     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
308238     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.92s 
308239     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_upper_bound 
309226     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_upper_bound 
309270     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 40.12ms 
309279     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_lower_bound.proof 
309281     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 2.05ms 
309282     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
312241     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.96s 
312241     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_lower_bound 
313224     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_lower_bound 
313264     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 36.15ms 
313267     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_positive_lower_bound_element.proof 
313268     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 260.9ns 
313269     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
316274     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3s 
316274     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_positive_lower_bound_element 
317249     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_positive_lower_bound_element 
317293     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 38.89ms 
317295     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_sub_same_index.proof 
317295     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 107.7ns 
317295     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
320192     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.9s 
320192     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_sub_same_index 
321126     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_sub_same_index 
321153     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 23.21ms 
321154     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_less_same_index.proof 
321154     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 89.6ns 
321155     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
324198     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.04s 
324198     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_less_same_index 
325155     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_less_same_index 
325204     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 44.24ms 
325207     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_equal_except_one_index.proof 
325207     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 245ns 
325208     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
328229     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.02s 
328229     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_equal_except_one_index 
329187     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_equal_except_one_index 
329213     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 21.55ms 
329215     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_is_max.proof 
329215     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 94.8ns 
329216     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
332282     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.07s 
332282     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_is_max 
333291     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_is_max 
333312     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 17.47ms 
333313     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_is_max2.proof 
333313     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 93.9ns 
333314     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
336296     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.98s 
336296     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_is_max2 
337278     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_is_max2 
337304     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 22.25ms 
337306     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_is_max3.proof 
337307     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 344.8ns 
337308     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
340367     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.06s 
340367     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_is_max3 
341341     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_is_max3 
341361     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 17.15ms 
341362     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_is_max4.proof 
341362     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 68.7ns 
341363     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
344506     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.14s 
344506     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_is_max4 
345457     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_is_max4 
345481     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 20.61ms 
345483     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_lt_max.proof 
345483     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 82.8ns 
345484     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
348456     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.97s 
348457     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_lt_max 
349446     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_lt_max 
349470     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 20.8ms 
349473     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_lt_max2.proof 
349473     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 261.5ns 
349474     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
352515     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.04s 
352516     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_lt_max2 
353525     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_lt_max2 
353551     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 21.69ms 
353553     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_lt_max3.proof 
353553     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 77.2ns 
353554     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
356671     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.12s 
356671     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_lt_max3 
357637     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_lt_max3 
357660     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 18.5ms 
357662     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_lt_max4.proof 
357662     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 69.5ns 
357663     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
360614     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.95s 
360614     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_lt_max4 
361614     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_lt_max4 
361639     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 21.15ms 
361641     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_gt0.proof 
361642     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 275ns 
361643     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
364696     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.05s 
364697     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_gt0 
365692     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_gt0 
365718     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 22.81ms 
365721     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_gt0_alt.proof 
365721     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 151.2ns 
365722     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
368711     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.99s 
368712     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_gt0_alt 
369692     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_gt0_alt 
369717     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 22.19ms 
369720     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_add_concrete.proof 
369720     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 253ns 
369721     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
372744     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.02s 
372745     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_add_concrete 
373672     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_add_concrete 
373679     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 5.56ms 
373681     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bprod/Taclet_bprod_all_positive.proof 
373681     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 75.6ns 
373682     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
376686     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3s 
376686     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bprod_all_positive 
377660     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bprod_all_positive 
377677     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 13.92ms 
377680     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bprod/Taclet_bprod_split.proof 
377680     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 233.1ns 
377681     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
380616     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.94s 
380617     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bprod_split 
381587     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bprod_split 
381592     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.38ms 
381593     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powConcrete0.proof 
381593     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 84.8ns 
381594     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
384599     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.01s 
384599     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powConcrete0 
385548     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powConcrete0 
385551     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 806.5ns 
385553     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powConcrete1.proof 
385553     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 98.5ns 
385554     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
388580     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.03s 
388580     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powConcrete1 
389534     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powConcrete1 
389537     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 811.4ns 
389538     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powSplitFactor.proof 
389538     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 65.1ns 
389539     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
392524     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.98s 
392524     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powSplitFactor 
393490     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powSplitFactor 
393497     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.83ms 
393498     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powAdd.proof 
393498     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 88.9ns 
393499     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
396404     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.9s 
396404     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powAdd 
397395     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powAdd 
397402     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.86ms 
397404     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powMono.proof 
397404     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 121.4ns 
397405     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
400320     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.92s 
400320     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powMono 
401309     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powMono 
401323     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 11.24ms 
401324     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powMonoConcrete.proof 
401324     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 133.3ns 
401325     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
404246     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.92s 
404246     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powMonoConcrete 
405228     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powMonoConcrete 
405232     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.21ms 
405233     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powMonoConcreteRight.proof 
405233     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 85.2ns 
405234     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
408254     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.02s 
408254     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powMonoConcreteRight 
409155     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powMonoConcreteRight 
409157     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 732.2ns 
409159     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powPositive.proof 
409159     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 75.7ns 
409160     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
412063     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.9s 
412063     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powPositive 
413028     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powPositive 
413034     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.08ms 
413036     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powPositiveConcrete.proof 
413036     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 85.9ns 
413037     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
416042     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3s 
416042     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powPositiveConcrete 
416941     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powPositiveConcrete 
416943     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 677.3ns 
416944     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powGeq1Concrete.proof 
416944     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 63ns 
416945     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
419768     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.82s 
419768     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powGeq1Concrete 
420761     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powGeq1Concrete 
420763     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 634.3ns 
420765     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_pow2InIntLower.proof 
420765     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 125.3ns 
420765     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
423533     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.77s 
423533     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: pow2InIntLower 
424526     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: pow2InIntLower 
424529     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 645.9ns 
424530     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_pow2InIntUpper.proof 
424530     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 76.1ns 
424531     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
427429     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.9s 
427429     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: pow2InIntUpper 
428435     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: pow2InIntUpper 
428439     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.19ms 
428441     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logSelfConcrete.proof 
428441     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 70.2ns 
428442     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
431438     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3s 
431438     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logSelfConcrete 
432399     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logSelfConcrete 
432408     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 7.09ms 
432410     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_log1Concrete.proof 
432410     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 84.9ns 
432410     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
435358     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.95s 
435358     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: log1Concrete 
436322     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: log1Concrete 
436326     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.97ms 
436327     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logProduct.proof 
436327     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 92.6ns 
436328     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
439289     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.96s 
439289     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logProduct 
440207     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logProduct 
440214     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.61ms 
440215     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logTimesBaseConcrete.proof 
440215     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 77.7ns 
440216     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
443125     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.91s 
443125     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logTimesBaseConcrete 
444128     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logTimesBaseConcrete 
444133     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.04ms 
444141     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logProdIdentity.proof 
444142     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 147.1ns 
444142     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
447051     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.91s 
447051     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logProdIdentity 
448015     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logProdIdentity 
448031     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 13.13ms 
448033     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logProdIdentityConcrete.proof 
448033     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 107.1ns 
448034     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
450921     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.89s 
450921     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logProdIdentityConcrete 
451877     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logProdIdentityConcrete 
451881     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.1ms 
451883     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logPowIdentity.proof 
451884     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 71.5ns 
451884     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
454806     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.92s 
454806     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logPowIdentity 
455727     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logPowIdentity 
455731     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.43ms 
455732     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logPowIdentityConcrete.proof 
455732     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 61.2ns 
455733     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
458735     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3s 
458736     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logPowIdentityConcrete 
459733     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logPowIdentityConcrete 
459737     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.32ms 
459739     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logPositive.proof 
459739     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 82.7ns 
459739     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
462743     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3s 
462743     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logPositive 
463745     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logPositive 
463763     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 15.42ms 
463765     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logPositiveConcrete.proof 
463765     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 93.6ns 
463767     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
466775     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.01s 
466775     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logPositiveConcrete 
467778     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logPositiveConcrete 
467783     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 410.9ns 
467786     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logMono.proof 
467786     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 246.6ns 
467788     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
470720     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.93s 
470720     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logMono 
471685     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logMono 
471723     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 33.2ms 
471725     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logMonoConcrete.proof 
471725     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 67.5ns 
471725     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
474730     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3s 
474731     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logMonoConcrete 
475714     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logMonoConcrete 
475720     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.99ms 
475724     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powLogLess.proof 
475724     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 262.4ns 
475725     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
478707     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.98s 
478707     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powLogLess 
479676     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powLogLess 
479698     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 19.32ms 
479699     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powLogMore2.proof 
479700     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 68.7ns 
479700     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
482722     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.02s 
482722     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powLogMore2 
483678     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powLogMore2 
483698     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 16.9ms 
483699     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logLessThanPow.proof 
483699     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 69.7ns 
483700     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
486680     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.98s 
486680     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logLessThanPow 
487608     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logLessThanPow 
487670     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 58.62ms 
487672     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logLessThanPowConcrete.proof 
487672     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 80.5ns 
487673     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
490675     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3s 
490675     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logLessThanPowConcrete 
491636     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logLessThanPowConcrete 
491638     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 626.4ns 
491640     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logSqueeze.proof 
491640     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 83.6ns 
491640     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
494550     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.91s 
494550     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logSqueeze 
495536     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logSqueeze 
495542     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.41ms 
495544     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/booleanRules/Taclet_ifthenelse_equals.proof 
495544     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 60.2ns 
495544     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
498615     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.07s 
498616     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: ifthenelse_equals 
499599     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: ifthenelse_equals 
499603     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.78ms 
499604     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/booleanRules/Taclet_ifthenelse_equals_1.proof 
499604     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 64.4ns 
499605     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
502540     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.94s 
502541     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: ifthenelse_equals_1 
503516     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: ifthenelse_equals_1 
503519     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 977.2ns 
503522     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/booleanRules/Taclet_ifthenelse_equals_2.proof 
503522     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 156ns 
503523     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
506623     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.1s 
506623     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: ifthenelse_equals_2 
507577     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: ifthenelse_equals_2 
507579     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 928.7ns 
507581     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/locSet/Taclet_disjointWithSingleton1.proof 
507581     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 56.9ns 
507581     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
510555     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.97s 
510555     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: disjointWithSingleton1 
511546     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: disjointWithSingleton1 
511550     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.7ms 
511551     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/locSet/Taclet_disjointWithSingleton2.proof 
511551     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 62ns 
511552     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
514515     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.96s 
514515     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: disjointWithSingleton2 
515497     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: disjointWithSingleton2 
515501     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.53ms 
515502     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/locSet/Taclet_disjointArrayRanges.proof 
515503     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 64.4ns 
515503     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
518475     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.97s 
518476     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: disjointArrayRanges 
519459     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: disjointArrayRanges 
519469     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 7.61ms 
519470     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/locSet/Taclet_disjointArrayRangeAllFields1.proof 
519470     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 72.4ns 
519471     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
522546     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.07s 
522546     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: disjointArrayRangeAllFields1 
523547     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: disjointArrayRangeAllFields1 
523557     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 6.73ms 
523560     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/locSet/Taclet_disjointArrayRangeAllFields2.proof 
523560     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 234.3ns 
523561     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
526562     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3s 
526562     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: disjointArrayRangeAllFields2 
527573     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: disjointArrayRangeAllFields2 
527584     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 8.4ms 
527585     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqSelfDefinition.proof 
527585     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 75.5ns 
527586     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
530621     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.03s 
530621     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqSelfDefinition 
531605     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqSelfDefinition 
531616     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 7.67ms 
531617     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqOutsideValue.proof 
531617     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 75.3ns 
531618     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
534619     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3s 
534619     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqOutsideValue 
535578     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqOutsideValue 
535583     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.78ms 
535584     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_castedGetAny.proof 
535584     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 73.5ns 
535585     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
538513     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.93s 
538514     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: castedGetAny 
539425     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: castedGetAny 
539430     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.11ms 
539432     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqGetAlphaCast.proof 
539432     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 73.5ns 
539432     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
542528     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.1s 
542529     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqGetAlphaCast 
543466     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqGetAlphaCast 
543469     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 910.6ns 
543471     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqSingleton.proof 
543471     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 68.9ns 
543472     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
546439     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.97s 
546439     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqSingleton 
547417     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqSingleton 
547420     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.13ms 
547421     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqSingletonConcrete.proof 
547421     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 67.8ns 
547422     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
550333     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.91s 
550333     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqSingletonConcrete 
551369     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqSingletonConcrete 
551372     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 996.2ns 
551373     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqConcat.proof 
551373     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 90.2ns 
551374     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
554278     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.9s 
554279     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqConcat 
555293     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqConcat 
555304     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 9.42ms 
555306     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqSub.proof 
555306     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 73.2ns 
555307     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
558246     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.94s 
558247     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqSub 
559168     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqSub 
559171     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.73ms 
559172     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqReverse.proof 
559172     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 73.7ns 
559173     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
562090     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.92s 
562091     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqReverse 
563065     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqReverse 
563072     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.61ms 
563074     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqEmpty.proof 
563074     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 69.2ns 
563074     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
566080     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.01s 
566080     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqEmpty 
567066     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqEmpty 
567069     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 856.3ns 
567071     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqSingleton.proof 
567071     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 66.8ns 
567071     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
569971     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.9s 
569971     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqSingleton 
570904     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqSingleton 
570906     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 697ns 
570907     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqConcat.proof 
570908     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 67.8ns 
570908     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
573757     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.85s 
573758     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqConcat 
574744     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqConcat 
574748     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.86ms 
574749     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqSub.proof 
574749     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 74.7ns 
574750     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
577672     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.92s 
577672     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqSub 
578687     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqSub 
578690     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.15ms 
578692     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqReverse.proof 
578692     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 57.3ns 
578692     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
581692     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3s 
581692     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqReverse 
582652     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqReverse 
582656     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.02ms 
582658     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_equalityToSeqGetAndSeqLenLeft.proof 
582658     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 97.9ns 
582659     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
585629     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.97s 
585629     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: equalityToSeqGetAndSeqLenLeft 
586661     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: equalityToSeqGetAndSeqLenLeft 
586664     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.36ms 
586665     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_equalityToSeqGetAndSeqLenRight.proof 
586665     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 82.9ns 
586666     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
589591     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.92s 
589591     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: equalityToSeqGetAndSeqLenRight 
590593     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: equalityToSeqGetAndSeqLenRight 
590597     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.76ms 
590599     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqSingletonEQ.proof 
590599     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 52.3ns 
590600     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
593538     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.94s 
593538     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqSingletonEQ 
594576     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqSingletonEQ 
594579     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.11ms 
594581     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqConcatEQ.proof 
594581     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 60.2ns 
594582     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
597625     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.04s 
597625     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqConcatEQ 
598597     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqConcatEQ 
598608     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 8.74ms 
598609     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqSubEQ.proof 
598609     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 64.8ns 
598610     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
601586     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.98s 
601587     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqSubEQ 
602542     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqSubEQ 
602545     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 884ns 
602546     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqReverseEQ.proof 
602546     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 82.8ns 
602547     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
605545     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3s 
605546     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqReverseEQ 
606573     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqReverseEQ 
606580     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 5.26ms 
606582     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqEmptyEQ.proof 
606582     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 55.8ns 
606583     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
609519     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.94s 
609519     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqEmptyEQ 
610544     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqEmptyEQ 
610547     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 998.3ns 
610549     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqSingletonEQ.proof 
610549     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 62.2ns 
610549     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
613546     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3s 
613546     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqSingletonEQ 
614562     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqSingletonEQ 
614565     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 974.1ns 
614566     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqConcatEQ.proof 
614567     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 98.5ns 
614568     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
617599     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.03s 
617600     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqConcatEQ 
618598     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqConcatEQ 
618602     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.43ms 
618604     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqSubEQ.proof 
618604     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 55.1ns 
618604     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
621598     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.99s 
621598     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqSubEQ 
622603     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqSubEQ 
622606     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.28ms 
622608     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqReverseEQ.proof 
622608     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 120.4ns 
622609     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
625652     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.04s 
625652     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqReverseEQ 
626685     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqReverseEQ 
626689     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.66ms 
626690     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqDefEQ.proof 
626690     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 77.3ns 
626691     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
629680     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.99s 
629680     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqDefEQ 
630645     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqDefEQ 
630648     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.37ms 
630649     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqDefEQ.proof 
630649     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 56.3ns 
630650     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
633637     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.99s 
633637     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqDefEQ 
634593     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqDefEQ 
634597     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.56ms 
634599     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqConcatWithSeqEmpty1.proof 
634599     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 71.1ns 
634600     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
637555     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.96s 
637555     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqConcatWithSeqEmpty1 
638502     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqConcatWithSeqEmpty1 
638511     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 6.78ms 
638513     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqConcatWithSeqEmpty2.proof 
638513     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 81.2ns 
638513     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
641502     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.99s 
641502     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqConcatWithSeqEmpty2 
642510     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqConcatWithSeqEmpty2 
642520     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 7.76ms 
642521     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqReverseOfSeqEmpty.proof 
642521     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 69.3ns 
642522     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
645460     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.94s 
645460     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqReverseOfSeqEmpty 
646433     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqReverseOfSeqEmpty 
646478     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 42.32ms 
646480     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_subSeqComplete.proof 
646480     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 58.8ns 
646480     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
649504     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.02s 
649504     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: subSeqComplete 
650511     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: subSeqComplete 
650520     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 6.16ms 
650521     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_subSeqTailR.proof 
650521     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 75.1ns 
650522     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
653530     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.01s 
653530     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: subSeqTailR 
654576     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: subSeqTailR 
654593     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 14.43ms 
654594     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_subSeqTailL.proof 
654594     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 70.8ns 
654595     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
657574     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.98s 
657574     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: subSeqTailL 
658601     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: subSeqTailL 
658616     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 12.12ms 
658617     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_subSeqTailEQR.proof 
658617     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 70.8ns 
658618     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
661661     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.04s 
661661     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: subSeqTailEQR 
662688     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: subSeqTailEQR 
662702     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 10.81ms 
662703     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_subSeqTailEQL.proof 
662703     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 55.4ns 
662704     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
665635     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.93s 
665636     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: subSeqTailEQL 
666586     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: subSeqTailEQL 
666595     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 6.91ms 
666596     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDef_split.proof 
666596     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 58.7ns 
666597     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
669548     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.95s 
669548     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_split 
670559     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDef_split 
670588     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 25.54ms 
670589     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDef_induction_upper.proof 
670590     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 128ns 
670590     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
673547     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.96s 
673547     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_induction_upper 
674550     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDef_induction_upper 
674576     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 23.16ms 
674577     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDef_induction_upper_concrete.proof 
674578     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 63.7ns 
674578     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
677544     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.97s 
677544     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_induction_upper_concrete 
678577     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDef_induction_upper_concrete 
678611     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 31.06ms 
678614     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDef_induction_lower.proof 
678614     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 312.6ns 
678615     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
681506     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.89s 
681506     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_induction_lower 
682459     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDef_induction_lower 
682485     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 22.55ms 
682486     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDef_induction_lower_concrete.proof 
682487     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 91ns 
682487     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
685481     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.99s 
685481     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_induction_lower_concrete 
686388     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDef_induction_lower_concrete 
686416     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 24.84ms 
686417     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDef_split_in_three.proof 
686417     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 76.1ns 
686418     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
689367     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.95s 
689367     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_split_in_three 
690275     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDef_split_in_three 
690336     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 54.01ms 
690337     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDef_empty.proof 
690337     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 203.7ns 
690338     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
693236     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.9s 
693236     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_empty 
694201     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDef_empty 
694207     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.32ms 
694208     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDef_one_summand.proof 
694208     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 50.3ns 
694209     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
697135     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.93s 
697135     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_one_summand 
698120     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDef_one_summand 
698126     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.21ms 
698127     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDef_lower_equals_upper.proof 
698127     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 63.4ns 
698128     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
701105     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.98s 
701105     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_lower_equals_upper 
702124     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDef_lower_equals_upper 
702129     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.43ms 
702130     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDefOfSeq.proof 
702130     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 65.9ns 
702131     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
705066     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.94s 
705066     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDefOfSeq 
706034     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDefOfSeq 
706052     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 14.85ms 
706054     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqSelfDefinitionEQ2.proof 
706054     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 69.4ns 
706055     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
709029     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.97s 
709029     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqSelfDefinitionEQ2 
709971     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqSelfDefinitionEQ2 
709983     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 9.54ms 
709986     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_indexOfSeqSingleton.proof 
709986     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 235.9ns 
709987     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
712844     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.86s 
712845     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: indexOfSeqSingleton 
713846     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: indexOfSeqSingleton 
713850     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.84ms 
713851     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_indexOfSeqConcatFirst.proof 
713851     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 68.6ns 
713852     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
716804     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.95s 
716805     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: indexOfSeqConcatFirst 
717784     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: indexOfSeqConcatFirst 
717797     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 10.17ms 
717798     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_indexOfSeqConcatSecond.proof 
717798     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 70.6ns 
717799     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
720730     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.93s 
720730     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: indexOfSeqConcatSecond 
721751     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: indexOfSeqConcatSecond 
721766     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 11.83ms 
721767     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_indexOfSeqSub.proof 
721767     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 73.9ns 
721768     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
724796     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.03s 
724797     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: indexOfSeqSub 
725807     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: indexOfSeqSub 
725825     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 14.69ms 
725826     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfArray2seq.proof 
725826     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 63.6ns 
725827     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
728857     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.03s 
728857     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfArray2seq 
729863     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfArray2seq 
729866     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.46ms 
729867     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getAnyOfArray2seq.proof 
729867     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 63.6ns 
729868     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
732902     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.03s 
732902     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getAnyOfArray2seq 
733863     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getAnyOfArray2seq 
733868     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.45ms 
733869     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfArray2seq.proof 
733869     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 56.9ns 
733870     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
736873     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3s 
736873     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfArray2seq 
737898     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfArray2seq 
737905     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.74ms 
737907     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_getAnyOfNPermInv.proof 
737907     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 77.5ns 
737908     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
740809     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.9s 
740810     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getAnyOfNPermInv 
741805     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getAnyOfNPermInv 
741811     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.38ms 
741812     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqNPermRange.proof 
741812     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 69.5ns 
741813     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
744867     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.05s 
744867     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqNPermRange 
745885     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqNPermRange 
745945     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 53.19ms 
745947     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermTrans.proof 
745947     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 91ns 
745947     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
748941     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.99s 
748941     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermTrans 
749905     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermTrans 
749929     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 20.49ms 
749930     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermRefl.proof 
749930     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 65.4ns 
749931     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
752873     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.94s 
752873     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermRefl 
753875     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermRefl 
753891     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 13.79ms 
753893     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermSplit.proof 
753893     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 65.4ns 
753894     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
756873     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.98s 
756873     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermSplit 
757907     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermSplit 
757909     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 189.8ns 
757910     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqNPermRight.proof 
757910     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 74.6ns 
757912     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
760998     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.09s 
760998     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqNPermRight 
762006     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqNPermRight 
762125     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 106.33ms 
762127     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermFromSwap.proof 
762127     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 130.9ns 
762128     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
765157     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.03s 
765157     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermFromSwap 
766106     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermFromSwap 
766154     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 42.81ms 
766156     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermTransAlt0.proof 
766156     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 77.3ns 
766157     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
769217     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.06s 
769217     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermTransAlt0 
770215     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermTransAlt0 
770217     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 233.5ns 
770219     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermTransAlt1.proof 
770220     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 271.9ns 
770220     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
773193     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.97s 
773193     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermTransAlt1 
774226     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermTransAlt1 
774228     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 276.2ns 
774229     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermTransAlt2.proof 
774230     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 68.7ns 
774230     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
777233     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3s 
777233     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermTransAlt2 
778227     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermTransAlt2 
778229     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 243.8ns 
778230     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermTransAlt3.proof 
778230     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 61.7ns 
778231     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
781175     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.94s 
781175     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermTransAlt3 
782118     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermTransAlt3 
782120     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 478.6ns 
782121     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermForall.proof 
782121     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 68.5ns 
782122     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
785088     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.97s 
785088     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermForall 
786070     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermForall 
786172     INFO  Test worker     d.u.i.k.s.SMTFocusResults Analyzing unsat core: (L_1 L_3 L_4) 
786181     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 108.89ms 
786184     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermExists.proof 
786184     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 238.7ns 
786185     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
789146     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.96s 
789146     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermExists 
790171     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermExists 
790221     INFO  Test worker     d.u.i.k.s.SMTFocusResults Analyzing unsat core: (L_1 L_3 L_5 L_6 L_7) 
790222     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 48.43ms 
790225     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm2/Taclet_schiffl_lemma_2.proof 
790225     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 73.8ns 
790226     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
793286     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.06s 
793286     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: schiffl_lemma_2 
794322     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: schiffl_lemma_2 
794323     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.6ns 
794363     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [1] goal: 0, source line: 49, command: 'macro split-prop' 
794402     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [2] goal: 3, source line: 50, command: 'rule allRight' 
794417     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [3] goal: 4, source line: 51, command: 'rule allRight' 
794423     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [4] goal: 5, source line: 52, command: 'macro split-prop' 
794436     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [5] goal: 11, source line: 53, command: 'rule 'seqPermDefLeft'' 
794437     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [6] goal: 12, source line: 54, command: 'rule 'andLeft'' 
794440     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [7] goal: 13, source line: 55, command: 'rule 'exLeft'' 
794441     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [8] goal: 14, source line: 56, command: 'macro split-prop' 
794446     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [9] goal: 16, source line: 57, command: 'rule  seqNPermRange' 
794448     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' 
794450     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [11] goal: 18, source line: 60, command: 'rule impLeft' 
794452     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [12] goal: 19, source line: 61, command: 'tryclose branch' 
794711     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [13] goal: 20, source line: 62, command: 'rule andLeft' 
794713     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [14] goal: 97, source line: 63, command: 'rule andLeft' 
794714     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' 
794715     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [16] goal: 99, source line: 66, command: 'rule impLeft' 
794717     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [17] goal: 100, source line: 67, command: 'tryclose branch' 
794849     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [18] goal: 101, source line: 68, command: 'rule andLeft' 
794851     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [19] goal: 188, source line: 69, command: 'rule andLeft' 
794852     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [20] goal: 189, source line: 70, command: 'rule seqNPermDefLeft' 
794853     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' 
794855     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [22] goal: 191, source line: 73, command: 'rule impLeft' 
794857     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [23] goal: 192, source line: 74, command: 'tryclose branch' 
795061     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [24] goal: 193, source line: 75, command: 'rule exLeft' 
795062     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [25] goal: 310, source line: 76, command: 'rule andLeft' 
795063     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [26] goal: 311, source line: 77, command: 'rule andLeft' 
795064     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' 
795065     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [28] goal: 313, source line: 80, command: 'rule impLeft' 
795066     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [29] goal: 314, source line: 81, command: 'tryclose branch' 
795216     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [30] goal: 315, source line: 82, command: 'rule exLeft' 
795217     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [31] goal: 420, source line: 83, command: 'rule andLeft' 
795219     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [32] goal: 421, source line: 84, command: 'rule andLeft' 
795220     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' 
795220     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [34] goal: 423, source line: 87, command: 'rule impLeft' 
795222     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [35] goal: 424, source line: 88, command: 'tryclose branch' 
795230     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [36] goal: 425, source line: 89, command: 'rule andLeft' 
795231     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [37] goal: 434, source line: 90, command: 'rule andLeft' 
795233     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' 
795234     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' 
795235     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [40] goal: 437, source line: 94, command: 'rule impLeft' 
795236     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [41] goal: 438, source line: 95, command: 'tryclose branch' 
795245     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [42] goal: 439, source line: 96, command: 'rule andLeft' 
795246     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [43] goal: 448, source line: 97, command: 'rule andLeft' 
795247     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' 
795248     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [45] goal: 450, source line: 99, command: 'instantiate var=iv  with='v_x_0'' 
795249     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [46] goal: 451, source line: 101, command: 'rule impLeft' 
795250     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [47] goal: 452, source line: 102, command: 'tryclose branch' 
795410     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [48] goal: 453, source line: 103, command: 'instantiate var=iv  with='v_y_0'' 
795411     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [49] goal: 562, source line: 105, command: 'rule impLeft' 
795412     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [50] goal: 563, source line: 106, command: 'tryclose branch' 
795570     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [51] goal: 564, source line: 107, command: 'cut 'v_x_0 = v_y_0'' 
795571     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)'' 
795573     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [53] goal: 676, source line: 111, command: 'rule andRight' 
795575     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [54] goal: 677, source line: 113, command: 'rule andRight' 
795576     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [55] goal: 679, source line: 114, command: 'rule andRight' 
795577     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [56] goal: 681, source line: 115, command: 'rule andRight' 
795578     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [57] goal: 683, source line: 116, command: 'rule lenOfSwap' 
795579     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [58] goal: 685, source line: 117, command: 'tryclose branch' 
795584     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [59] goal: 684, source line: 118, command: 'rule seqNPermSwapNPerm' 
795585     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' 
795587     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [61] goal: 688, source line: 121, command: 'instantiate hide var='jv' with='jv_0'' 
795588     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [62] goal: 689, source line: 122, command: 'rule impLeft' 
795589     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [63] goal: 690, source line: 123, command: 'tryclose branch' 
795730     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [64] goal: 691, source line: 124, command: 'tryclose branch' 
795735     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [65] goal: 682, source line: 125, command: 'rule allRight' 
795736     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [66] goal: 796, source line: 127, command: 'rule impRight' 
795738     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [67] goal: 797, source line: 128, command: 'rule andLeft' 
795739     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [68] goal: 798, source line: 129, command: 'instantiate var=iv with='v_iv_0'' 
795740     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [69] goal: 799, source line: 130, command: 'rule impLeft' 
795741     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [70] goal: 800, source line: 131, command: 'tryclose branch' 
795901     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [71] goal: 801, source line: 132, command: 'rule getOfSwap' 
795903     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [72] goal: 912, source line: 133, command: 'rule ifthenelse_negated' 
795904     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [73] goal: 913, source line: 134, command: 'rule ifthenelse_split occ=0' 
795906     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [74] goal: 914, source line: 135, command: 'rule andLeft' 
795907     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [75] goal: 916, source line: 136, command: 'rule andLeft' 
795907     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [76] goal: 917, source line: 137, command: 'rule andLeft' 
795908     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [77] goal: 918, source line: 138, command: 'rule ifthenelse_split occ=0' 
795909     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [78] goal: 919, source line: 139, command: 'tryclose branch' 
796040     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [79] goal: 920, source line: 140, command: 'rule ifthenelse_split occ=0' 
796042     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [80] goal: 1011, source line: 141, command: 'tryclose branch' 
796167     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [81] goal: 1012, source line: 142, command: 'tryclose branch' 
796173     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [82] goal: 915, source line: 143, command: 'tryclose branch' 
796178     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [83] goal: 680, source line: 144, command: 'rule getOfSwap' 
796179     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [84] goal: 1099, source line: 146, command: 'rule ifthenelse_negated' 
796180     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [85] goal: 1100, source line: 147, command: 'rule ifthenelse_split occ=0' 
796181     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [86] goal: 1101, source line: 148, command: 'rule andLeft' 
796182     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [87] goal: 1103, source line: 149, command: 'rule andLeft' 
796183     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [88] goal: 1104, source line: 150, command: 'rule andLeft' 
796184     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [89] goal: 1105, source line: 151, command: 'rule ifthenelse_split occ=0' 
796184     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [90] goal: 1106, source line: 152, command: 'tryclose branch' 
796195     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [91] goal: 1107, source line: 153, command: 'tryclose branch' 
796201     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [92] goal: 1102, source line: 154, command: 'tryclose branch' 
796332     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [93] goal: 678, source line: 155, command: 'rule getOfSwap' 
796333     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [94] goal: 1225, source line: 157, command: 'rule ifthenelse_negated' 
796335     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [95] goal: 1226, source line: 158, command: 'rule ifthenelse_split occ=0' 
796336     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [96] goal: 1227, source line: 159, command: 'rule andLeft' 
796337     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [97] goal: 1229, source line: 160, command: 'rule andLeft' 
796337     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [98] goal: 1230, source line: 161, command: 'rule andLeft' 
796338     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [99] goal: 1231, source line: 162, command: 'rule ifthenelse_split occ=0' 
796338     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [100] goal: 1232, source line: 163, command: 'tryclose branch' 
796404     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [101] goal: 1233, source line: 164, command: 'tryclose branch' 
796412     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [102] goal: 1228, source line: 165, command: 'tryclose branch' 
796544     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]'' 
796545     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [104] goal: 1397, source line: 169, command: 'rule seqNPermInjective' 
796546     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'' 
796547     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'' 
796549     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [107] goal: 1401, source line: 172, command: 'rule impLeft' 
796550     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [108] goal: 1402, source line: 173, command: 'tryclose branch' 
796743     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [109] goal: 1403, source line: 174, command: 'tryclose branch' 
796748     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'' 
796749     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)'' 
796750     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [112] goal: 1536, source line: 179, command: 'rule andRight' 
796752     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [113] goal: 1537, source line: 181, command: 'rule andRight' 
796753     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [114] goal: 1539, source line: 182, command: 'rule andRight' 
796754     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [115] goal: 1541, source line: 183, command: 'rule andRight' 
796754     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [116] goal: 1543, source line: 184, command: 'tryclose branch' 
796767     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [117] goal: 1544, source line: 185, command: 'rule seqNPermSwapNPerm' 
796768     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'' 
796770     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [119] goal: 1559, source line: 188, command: 'instantiate hide var=jv with='jv_1'' 
796771     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [120] goal: 1560, source line: 189, command: 'tryclose branch' 
796922     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [121] goal: 1542, source line: 190, command: 'rule allRight' 
796924     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [122] goal: 1667, source line: 192, command: 'rule impRight' 
796925     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [123] goal: 1668, source line: 193, command: 'rule andLeft' 
796926     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [124] goal: 1669, source line: 194, command: 'instantiate var=iv with='v_iv_0'' 
796928     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [125] goal: 1670, source line: 195, command: 'rule impLeft' 
796929     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [126] goal: 1671, source line: 196, command: 'tryclose branch' 
797054     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [127] goal: 1672, source line: 197, command: 'rule getOfSwap' 
797056     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [128] goal: 1786, source line: 198, command: 'rule ifthenelse_negated' 
797057     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [129] goal: 1787, source line: 199, command: 'rule ifthenelse_split occ=0' 
797058     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [130] goal: 1788, source line: 200, command: 'rule andLeft' 
797059     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [131] goal: 1790, source line: 201, command: 'rule andLeft' 
797060     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [132] goal: 1791, source line: 202, command: 'rule andLeft' 
797061     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [133] goal: 1792, source line: 203, command: 'rule ifthenelse_split occ=0' 
797061     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [134] goal: 1793, source line: 204, command: 'tryclose branch' 
797172     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [135] goal: 1794, source line: 205, command: 'rule ifthenelse_split occ=0' 
797174     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [136] goal: 1885, source line: 206, command: 'tryclose branch' 
797276     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [137] goal: 1886, source line: 207, command: 'instantiate var=iv with='v_y_0'' 
797278     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [138] goal: 1968, source line: 208, command: 'rule impLeft' 
797279     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [139] goal: 1969, source line: 209, command: 'tryclose branch' 
797284     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [140] goal: 1970, source line: 210, command: 'tryclose branch' 
797290     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [141] goal: 1789, source line: 211, command: 'tryclose branch' 
797296     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [142] goal: 1540, source line: 212, command: 'tryclose branch' 
797449     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [143] goal: 1538, source line: 213, command: 'rule getOfSwap' 
797450     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [144] goal: 2097, source line: 215, command: 'rule ifthenelse_negated' 
797451     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [145] goal: 2098, source line: 216, command: 'rule ifthenelse_split occ=0' 
797452     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [146] goal: 2099, source line: 217, command: 'tryclose branch' 
797466     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [147] goal: 2100, source line: 218, command: 'tryclose branch' 
797576     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [148] goal: 1535, source line: 219, command: 'tryclose branch' 
801712     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'' 
801713     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)'' 
801718     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [151] goal: 4268, source line: 226, command: 'rule andRight' 
801719     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [152] goal: 4269, source line: 228, command: 'rule andRight' 
801720     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [153] goal: 4271, source line: 229, command: 'rule andRight' 
801721     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [154] goal: 4273, source line: 230, command: 'rule andRight' 
801722     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [155] goal: 4275, source line: 231, command: 'tryclose branch' 
801732     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [156] goal: 4276, source line: 232, command: 'rule seqNPermSwapNPerm' 
801732     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'' 
801735     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [158] goal: 4288, source line: 235, command: 'instantiate hide var=jv with='jv_0'' 
801736     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [159] goal: 4289, source line: 236, command: 'rule impLeft' 
801737     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [160] goal: 4290, source line: 237, command: 'tryclose branch' 
801855     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [161] goal: 4291, source line: 238, command: 'tryclose branch' 
801859     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [162] goal: 4274, source line: 239, command: 'rule allRight' 
801860     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [163] goal: 4400, source line: 241, command: 'rule impRight' 
801861     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [164] goal: 4401, source line: 242, command: 'rule andLeft' 
801862     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [165] goal: 4402, source line: 243, command: 'instantiate var=iv with='v_iv_0'' 
801863     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [166] goal: 4403, source line: 244, command: 'rule impLeft' 
801864     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [167] goal: 4404, source line: 245, command: 'tryclose branch' 
801985     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [168] goal: 4405, source line: 246, command: 'rule getOfSwap' 
801987     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [169] goal: 4521, source line: 247, command: 'rule ifthenelse_negated' 
801988     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [170] goal: 4522, source line: 248, command: 'rule ifthenelse_split occ=0' 
801989     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [171] goal: 4523, source line: 249, command: 'rule andLeft' 
801990     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [172] goal: 4525, source line: 250, command: 'rule andLeft' 
801991     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [173] goal: 4526, source line: 251, command: 'rule andLeft' 
801992     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [174] goal: 4527, source line: 252, command: 'rule ifthenelse_split occ=0' 
801992     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [175] goal: 4528, source line: 253, command: 'tryclose branch' 
802092     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [176] goal: 4529, source line: 254, command: 'rule ifthenelse_split occ=0' 
802093     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [177] goal: 4622, source line: 255, command: 'tryclose branch' 
802195     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [178] goal: 4623, source line: 256, command: 'tryclose branch' 
802201     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [179] goal: 4524, source line: 257, command: 'tryclose branch' 
802206     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [180] goal: 4272, source line: 258, command: 'rule getOfSwap' 
802207     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [181] goal: 4713, source line: 260, command: 'rule ifthenelse_negated' 
802208     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [182] goal: 4714, source line: 261, command: 'rule ifthenelse_split occ=0' 
802210     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [183] goal: 4715, source line: 262, command: 'tryclose branch' 
802223     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [184] goal: 4716, source line: 263, command: 'tryclose branch' 
802332     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [185] goal: 4270, source line: 264, command: 'rule getOfSwap' 
802333     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [186] goal: 4839, source line: 266, command: 'rule ifthenelse_negated' 
802334     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [187] goal: 4840, source line: 267, command: 'rule ifthenelse_split occ=0' 
802336     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [188] goal: 4841, source line: 268, command: 'tryclose branch' 
802437     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [189] goal: 4842, source line: 269, command: 'tryclose branch' 
802450     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'' 
802451     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)'' 
802452     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [192] goal: 4950, source line: 275, command: 'rule andRight' 
802453     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [193] goal: 4951, source line: 277, command: 'rule andRight' 
802454     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [194] goal: 4953, source line: 278, command: 'rule andRight' 
802455     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [195] goal: 4955, source line: 279, command: 'rule andRight' 
802456     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [196] goal: 4957, source line: 280, command: 'tryclose branch' 
802470     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [197] goal: 4958, source line: 281, command: 'rule seqNPermSwapNPerm' 
802471     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [198] goal: 4977, source line: 283, command: 'instantiate hide var=iv with='jv_0'' 
802472     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'' 
802473     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [200] goal: 4979, source line: 285, command: 'rule impLeft' 
802474     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [201] goal: 4980, source line: 286, command: 'tryclose branch' 
802586     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))'' 
802587     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [203] goal: 5093, source line: 288, command: 'instantiate hide var=iv with='jv_0'' 
802588     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'' 
802589     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [205] goal: 5095, source line: 290, command: 'rule impLeft' 
802590     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [206] goal: 5096, source line: 291, command: 'tryclose branch' 
802764     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [207] goal: 5097, source line: 292, command: 'tryclose branch' 
802770     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [208] goal: 4956, source line: 293, command: 'rule allRight' 
802771     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [209] goal: 5212, source line: 295, command: 'rule impRight' 
802772     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [210] goal: 5213, source line: 296, command: 'rule andLeft' 
802773     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [211] goal: 5214, source line: 297, command: 'instantiate var=iv with='v_iv_0'' 
802773     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [212] goal: 5215, source line: 300, command: 'rule impLeft' 
802774     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [213] goal: 5216, source line: 301, command: 'tryclose branch' 
802900     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [214] goal: 5217, source line: 302, command: 'rule getOfSwap' 
802900     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [215] goal: 5337, source line: 304, command: 'rule ifthenelse_negated' 
802902     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [216] goal: 5338, source line: 305, command: 'rule ifthenelse_split occ=0' 
802903     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [217] goal: 5339, source line: 306, command: 'rule andLeft' 
802903     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [218] goal: 5341, source line: 307, command: 'rule andLeft' 
802904     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [219] goal: 5342, source line: 308, command: 'rule andLeft' 
802905     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [220] goal: 5343, source line: 309, command: 'rule ifthenelse_split occ=0' 
802905     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [221] goal: 5344, source line: 310, command: 'rule getOfSwap' 
802906     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [222] goal: 5346, source line: 311, command: 'rule ifthenelse_negated' 
802907     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [223] goal: 5347, source line: 312, command: 'rule ifthenelse_split occ=0' 
802909     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [224] goal: 5348, source line: 313, command: 'rule andLeft' 
802910     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [225] goal: 5350, source line: 314, command: 'rule andLeft' 
802910     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [226] goal: 5351, source line: 315, command: 'rule andLeft' 
802911     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [227] goal: 5352, source line: 316, command: 'rule ifthenelse_split occ=0' 
802911     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [228] goal: 5353, source line: 317, command: 'tryclose branch' 
803022     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [229] goal: 5354, source line: 318, command: 'rule ifthenelse_split occ=0' 
803024     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [230] goal: 5463, source line: 319, command: 'tryclose branch' 
803032     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [231] goal: 5464, source line: 320, command: 'tryclose branch' 
803137     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [232] goal: 5349, source line: 321, command: 'tryclose branch' 
803240     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [233] goal: 5345, source line: 322, command: 'rule ifthenelse_split' 
803241     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [234] goal: 5660, source line: 324, command: 'rule getOfSwap' 
803242     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [235] goal: 5662, source line: 325, command: 'rule ifthenelse_negated' 
803243     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [236] goal: 5663, source line: 326, command: 'rule ifthenelse_split occ=0' 
803244     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [237] goal: 5664, source line: 327, command: 'rule andLeft' 
803245     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [238] goal: 5666, source line: 328, command: 'rule andLeft' 
803245     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [239] goal: 5667, source line: 329, command: 'rule andLeft' 
803245     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [240] goal: 5668, source line: 330, command: 'rule ifthenelse_split occ=0' 
803246     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [241] goal: 5669, source line: 331, command: 'tryclose branch' 
803357     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [242] goal: 5670, source line: 332, command: 'tryclose branch' 
803365     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [243] goal: 5665, source line: 333, command: 'tryclose branch' 
803476     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [244] goal: 5661, source line: 334, command: 'rule getOfSwap' 
803477     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [245] goal: 5887, source line: 336, command: 'rule ifthenelse_negated' 
803478     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [246] goal: 5888, source line: 337, command: 'rule ifthenelse_split occ=0' 
803479     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [247] goal: 5889, source line: 338, command: 'rule andLeft' 
803480     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [248] goal: 5891, source line: 339, command: 'rule andLeft' 
803480     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [249] goal: 5892, source line: 340, command: 'rule andLeft' 
803481     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [250] goal: 5893, source line: 341, command: 'rule ifthenelse_split occ=0' 
803482     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [251] goal: 5894, source line: 342, command: 'tryclose branch' 
803488     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [252] goal: 5895, source line: 343, command: 'rule ifthenelse_split occ=0' 
803489     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [253] goal: 5897, source line: 344, command: 'tryclose branch' 
803586     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [254] goal: 5898, source line: 345, command: 'tryclose branch' 
803592     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [255] goal: 5890, source line: 346, command: 'tryclose branch' 
803599     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [256] goal: 5340, source line: 347, command: 'tryclose branch' 
803729     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [257] goal: 4954, source line: 348, command: 'rule getOfSwap' 
803730     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [258] goal: 6115, source line: 350, command: 'rule ifthenelse_negated' 
803731     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [259] goal: 6116, source line: 351, command: 'rule ifthenelse_split occ=0' 
803732     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [260] goal: 6117, source line: 352, command: 'rule andLeft' 
803732     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [261] goal: 6119, source line: 353, command: 'rule andLeft' 
803733     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [262] goal: 6120, source line: 354, command: 'rule andLeft' 
803733     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [263] goal: 6121, source line: 355, command: 'rule ifthenelse_split occ=0' 
803734     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [264] goal: 6122, source line: 356, command: 'tryclose branch' 
803803     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [265] goal: 6123, source line: 357, command: 'rule ifthenelse_split occ=0' 
803804     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [266] goal: 6193, source line: 358, command: 'rule getOfSwap' 
803805     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [267] goal: 6195, source line: 359, command: 'rule ifthenelse_negated' 
803805     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [268] goal: 6196, source line: 360, command: 'rule ifthenelse_split occ=0' 
803806     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [269] goal: 6197, source line: 361, command: 'tryclose branch' 
803813     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [270] goal: 6198, source line: 362, command: 'tryclose branch' 
803820     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [271] goal: 6194, source line: 363, command: 'tryclose branch' 
803959     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [272] goal: 6118, source line: 364, command: 'tryclose branch' 
804071     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [273] goal: 4952, source line: 365, command: 'rule getOfSwap' 
804072     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [274] goal: 6456, source line: 367, command: 'rule ifthenelse_negated' 
804073     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [275] goal: 6457, source line: 368, command: 'rule ifthenelse_split occ=0' 
804074     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [276] goal: 6458, source line: 369, command: 'tryclose branch' 
804286     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [277] goal: 6459, source line: 370, command: 'tryclose branch' 
804399     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'' 
804400     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [279] goal: 6735, source line: 375, command: 'tryclose branch' 
807942     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [280] goal: 6735, source line: 378, command: 'rule seqNPermSwapNPerm' 
807947     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [281] goal: 8783, source line: 380, command: 'instantiate hide var=iv with='jv_1'' 
807948     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'' 
807948     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [283] goal: 8785, source line: 382, command: 'rule impLeft' 
807949     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [284] goal: 8786, source line: 383, command: 'tryclose branch' 
808074     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))'' 
808074     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [286] goal: 8909, source line: 385, command: 'instantiate hide var=iv with='jv_1'' 
808076     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'' 
808077     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [288] goal: 8911, source line: 387, command: 'rule impLeft' 
808078     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [289] goal: 8912, source line: 388, command: 'tryclose branch' 
808194     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [290] goal: 8913, source line: 389, command: 'tryclose branch' 
811666     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [291] goal: 6736, source line: 390, command: 'tryclose branch' 
815283     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [292] goal: 6736, source line: 397, command: 'rule seqNPermSwapNPerm formula='seqNPerm(s_0)'' 
815288     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'' 
815289     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [294] goal: 12634, source line: 400, command: 'instantiate hide var=jv with='jv_0'' 
815290     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [295] goal: 12635, source line: 401, command: 'rule impLeft' 
815291     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [296] goal: 12636, source line: 402, command: 'tryclose branch' 
815431     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))'' 
815431     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'' 
815432     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [299] goal: 12758, source line: 405, command: 'instantiate hide var=jv with='jv_1'' 
815434     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)' ...' 
815434     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [301] goal: 12760, source line: 407, command: 'tryclose branch' 
816678     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm2/Taclet_schiffl_thm_1.proof 
816678     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 106.4ns 
816679     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
819737     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.06s 
819737     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: schiffl_thm_1 
820678     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: schiffl_thm_1 
820679     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 6.6ns 
820680     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [1] goal: 0, source line: 50, command: 'macro split-prop' 
820688     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)'' 
820697     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [3] goal: 11, source line: 52, command: 'instantiate hide var=x with='f_x'' 
820700     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [4] goal: 12, source line: 53, command: 'instantiate hide var=y with='f_y'' 
820702     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [5] goal: 13, source line: 54, command: 'rule impLeft' 
820704     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [6] goal: 14, source line: 55, command: 'tryclose branch' 
820709     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [7] goal: 15, source line: 56, command: 'rule exLeft' 
820709     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [8] goal: 23, source line: 57, command: 'macro split-prop' 
820713     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [9] goal: 27, source line: 58, command: 'rule seqPermDef occ=1' 
820714     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [10] goal: 28, source line: 59, command: 'rule andRight' 
820716     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [11] goal: 29, source line: 60, command: 'tryclose branch' 
820727     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [12] goal: 30, source line: 61, command: 'instantiate hide var=s with='r_0'' 
820727     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [13] goal: 46, source line: 62, command: 'rule andRight' 
820729     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [14] goal: 47, source line: 63, command: 'tryclose branch' 
820786     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [15] goal: 48, source line: 64, command: 'rule allRight' 
820787     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [16] goal: 119, source line: 65, command: 'rule impRight' 
820787     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [17] goal: 120, source line: 66, command: 'instantiate hide var=iv with='iv_0'' 
820788     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [18] goal: 121, source line: 67, command: 'rule impLeft' 
820788     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [19] goal: 122, source line: 68, command: 'tryclose branch' 
820867     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [20] goal: 123, source line: 69, command: 'rule andLeft' 
820868     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [21] goal: 203, source line: 70, command: 'rule seqNPermRange' 
820868     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [22] goal: 204, source line: 71, command: 'instantiate hide var=iv with='iv_0'' 
820869     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [23] goal: 205, source line: 72, command: 'rule impLeft' 
820870     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [24] goal: 206, source line: 73, command: 'tryclose branch' 
820874     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [25] goal: 207, source line: 74, command: 'rule andLeft' 
820875     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [26] goal: 215, source line: 75, command: 'rule andLeft' 
820875     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [27] goal: 216, source line: 76, command: 'rule seqNPermRange' 
820876     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [28] goal: 217, source line: 77, command: 'instantiate hide var=iv with='f_x'' 
820877     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [29] goal: 218, source line: 78, command: 'rule impLeft' 
820877     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [30] goal: 219, source line: 79, command: 'tryclose branch' 
820973     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [31] goal: 220, source line: 80, command: 'rule andLeft' 
820973     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [32] goal: 311, source line: 81, command: 'rule andLeft' 
820974     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [33] goal: 312, source line: 82, command: 'rule seqNPermRange' 
820975     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [34] goal: 313, source line: 83, command: 'instantiate hide var=iv with='f_y'' 
820976     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [35] goal: 314, source line: 84, command: 'rule impLeft' 
820976     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [36] goal: 315, source line: 85, command: 'tryclose branch' 
821081     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [37] goal: 316, source line: 86, command: 'rule andLeft' 
821082     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [38] goal: 410, source line: 87, command: 'rule andLeft' 
821082     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [39] goal: 411, source line: 88, command: 'rule getOfSeqDef occ=0' 
821083     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [40] goal: 412, source line: 89, command: 'rule getOfSeqDef' 
821083     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [41] goal: 413, source line: 90, command: 'rule ifthenelse_split occ=0' 
821084     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [42] goal: 414, source line: 91, command: 'rule andLeft occ=0' 
821085     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [43] goal: 416, source line: 92, command: 'rule sub_zero_2 occ=0' 
821085     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [44] goal: 417, source line: 93, command: 'rule ifthenelse_split occ=2' 
821086     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [45] goal: 418, source line: 94, command: 'rule andLeft' 
821086     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [46] goal: 420, source line: 95, command: 'rule sub_zero_2 occ=0' 
821087     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [47] goal: 421, source line: 96, command: 'rule add_zero_right occ=0' 
821087     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [48] goal: 422, source line: 97, command: 'rule add_zero_right occ=0' 
821088     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [49] goal: 423, source line: 98, command: 'rule add_zero_right occ=0' 
821088     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [50] goal: 424, source line: 99, command: 'rule add_zero_right occ=0' 
821089     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [51] goal: 425, source line: 100, command: 'rule add_zero_right occ=0' 
821089     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [52] goal: 426, source line: 101, command: 'rule add_zero_right occ=0' 
821090     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [53] goal: 427, source line: 102, command: 'rule ifthenelse_split occ=0' 
821090     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [54] goal: 428, source line: 103, command: 'rule ifthenelse_split occ=0' 
821091     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [55] goal: 430, source line: 104, command: 'tryclose branch' 
821094     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [56] goal: 431, source line: 105, command: 'tryclose branch' 
821139     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [57] goal: 429, source line: 106, command: 'rule ifthenelse_split occ=0' 
821140     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [58] goal: 473, source line: 107, command: 'tryclose branch' 
821211     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [59] goal: 474, source line: 108, command: 'rule ifthenelse_split occ=0' 
821212     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [60] goal: 541, source line: 109, command: 'rule seqNPermInjective' 
821212     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [61] goal: 543, source line: 110, command: 'instantiate hide var=iv with='iv_0'' 
821214     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [62] goal: 544, source line: 111, command: 'instantiate hide var=jv with='f_y'' 
821215     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [63] goal: 545, source line: 112, command: 'rule impLeft' 
821215     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [64] goal: 546, source line: 113, command: 'tryclose branch' 
821279     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [65] goal: 547, source line: 114, command: 'tryclose branch' 
821282     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [66] goal: 542, source line: 115, command: 'rule ifthenelse_split occ=0' 
821282     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [67] goal: 606, source line: 116, command: 'rule seqNPermInjective' 
821283     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [68] goal: 608, source line: 117, command: 'instantiate hide var=iv with='iv_0'' 
821284     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [69] goal: 609, source line: 118, command: 'instantiate hide var=jv with='f_x'' 
821285     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [70] goal: 610, source line: 119, command: 'rule impLeft' 
821286     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [71] goal: 611, source line: 120, command: 'tryclose branch' 
821346     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [72] goal: 612, source line: 121, command: 'tryclose branch' 
821348     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [73] goal: 607, source line: 122, command: 'tryclose branch' 
821352     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [74] goal: 419, source line: 123, command: 'tryclose branch' 
821414     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [75] goal: 415, source line: 124, command: 'tryclose branch' 
821474     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_eqSameSeq.proof 
821475     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 95.3ns 
821476     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
824344     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.87s 
824344     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: eqSameSeq 
825390     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: eqSameSeq 
825414     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 19.46ms