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

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

tests
0

failures
0

ignored
10m45.11s

duration
100%

successful

Tests

Test Method name Duration Result
powPositive data()[100] 3.128s passed
powPositiveConcrete data()[101] 3.136s passed
powGeq1Concrete data()[102] 3.128s passed
pow2InIntLower data()[103] 3.113s passed
pow2InIntUpper data()[104] 3.103s passed
logSelfConcrete data()[105] 3.146s passed
log1Concrete data()[106] 3.114s passed
logProduct data()[107] 3.111s passed
logTimesBaseConcrete data()[108] 3.098s passed
logProdIdentity data()[109] 3.165s passed
moduloByteIsInByte data()[10] 3.204s passed
logProdIdentityConcrete data()[110] 3.133s passed
logPowIdentity data()[111] 3.122s passed
logPowIdentityConcrete data()[112] 3.130s passed
logPositive data()[113] 3.160s passed
logPositiveConcrete data()[114] 3.131s passed
logMono data()[115] 3.133s passed
logMonoConcrete data()[116] 3.137s passed
powLogLess data()[117] 3.139s passed
powLogMore2 data()[118] 3.124s passed
logLessThanPow data()[119] 3.147s passed
moduloCharIsInChar data()[11] 3.221s passed
logLessThanPowConcrete data()[120] 3.111s passed
logSqueeze data()[121] 3.107s passed
ifthenelse_equals data()[122] 3.126s passed
ifthenelse_equals_1 data()[123] 3.126s passed
ifthenelse_equals_2 data()[124] 3.107s passed
disjointWithSingleton1 data()[125] 3.139s passed
disjointWithSingleton2 data()[126] 3.116s passed
disjointArrayRanges data()[127] 3.151s passed
disjointArrayRangeAllFields1 data()[128] 3.142s passed
disjointArrayRangeAllFields2 data()[129] 3.137s passed
div_unique1 data()[12] 3.247s passed
seqSelfDefinition data()[130] 3.131s passed
seqOutsideValue data()[131] 3.144s passed
castedGetAny data()[132] 3.140s passed
seqGetAlphaCast data()[133] 3.138s passed
getOfSeqSingleton data()[134] 3.148s passed
getOfSeqSingletonConcrete data()[135] 3.115s passed
getOfSeqConcat data()[136] 3.138s passed
getOfSeqSub data()[137] 3.140s passed
getOfSeqReverse data()[138] 3.129s passed
lenOfSeqEmpty data()[139] 3.168s passed
div_unique2 data()[13] 3.248s passed
lenOfSeqSingleton data()[140] 3.135s passed
lenOfSeqConcat data()[141] 3.150s passed
lenOfSeqSub data()[142] 3.137s passed
lenOfSeqReverse data()[143] 3.165s passed
equalityToSeqGetAndSeqLenLeft data()[144] 3.161s passed
equalityToSeqGetAndSeqLenRight data()[145] 3.149s passed
getOfSeqSingletonEQ data()[146] 3.152s passed
getOfSeqConcatEQ data()[147] 3.140s passed
getOfSeqSubEQ data()[148] 3.154s passed
getOfSeqReverseEQ data()[149] 3.172s passed
div_exists data()[14] 3.359s passed
lenOfSeqEmptyEQ data()[150] 3.127s passed
lenOfSeqSingletonEQ data()[151] 3.133s passed
lenOfSeqConcatEQ data()[152] 3.148s passed
lenOfSeqSubEQ data()[153] 3.148s passed
lenOfSeqReverseEQ data()[154] 3.130s passed
getOfSeqDefEQ data()[155] 3.141s passed
lenOfSeqDefEQ data()[156] 3.157s passed
seqConcatWithSeqEmpty1 data()[157] 3.154s passed
seqConcatWithSeqEmpty2 data()[158] 3.149s passed
seqReverseOfSeqEmpty data()[159] 3.149s passed
div_one data()[15] 3.211s passed
subSeqComplete data()[160] 3.152s passed
subSeqTailR data()[161] 3.147s passed
subSeqTailL data()[162] 3.155s passed
subSeqTailEQR data()[163] 3.144s passed
subSeqTailEQL data()[164] 3.145s passed
seqDef_split data()[165] 3.151s passed
seqDef_induction_upper data()[166] 3.164s passed
seqDef_induction_upper_concrete data()[167] 3.164s passed
seqDef_induction_lower data()[168] 3.158s passed
seqDef_induction_lower_concrete data()[169] 3.157s passed
jdiv_one data()[16] 3.192s passed
seqDef_split_in_three data()[170] 3.190s passed
seqDef_empty data()[171] 3.144s passed
seqDef_one_summand data()[172] 3.172s passed
seqDef_lower_equals_upper data()[173] 3.150s passed
seqDefOfSeq data()[174] 3.167s passed
seqSelfDefinitionEQ2 data()[175] 3.161s passed
indexOfSeqSingleton data()[176] 3.158s passed
indexOfSeqConcatFirst data()[177] 3.159s passed
indexOfSeqConcatSecond data()[178] 3.165s passed
indexOfSeqSub data()[179] 3.156s passed
div_zero data()[17] 3.206s passed
lenOfArray2seq data()[180] 3.154s passed
getAnyOfArray2seq data()[181] 3.153s passed
getOfArray2seq data()[182] 3.154s passed
getAnyOfNPermInv data()[183] 3.168s passed
seqNPermRange data()[184] 3.192s passed
seqPermTrans data()[185] 3.196s passed
seqPermRefl data()[186] 3.149s passed
seqPermSplit data()[187] 3.140s passed
seqNPermRight data()[188] 3.240s passed
seqPermFromSwap data()[189] 3.180s passed
divResZero1 data()[18] 3.239s passed
seqPermTransAlt0 data()[190] 3.174s passed
seqPermTransAlt1 data()[191] 3.130s passed
seqPermTransAlt2 data()[192] 3.120s passed
seqPermTransAlt3 data()[193] 3.116s passed
seqPermForall data()[194] 3.238s passed
seqPermExists data()[195] 3.180s passed
schiffl_lemma_2 data()[196] 20.765s passed
schiffl_thm_1 data()[197] 3.950s passed
eqSameSeq data()[198] 3.440s passed
divResZero2 data()[19] 3.180s passed
eqTermCut data()[1] 3.852s passed
divResOne1 data()[20] 3.248s passed
divResOne2 data()[21] 3.251s passed
div_cancel1 data()[22] 3.204s passed
div_cancel2 data()[23] 3.164s passed
divAddMultDenom data()[24] 3.213s passed
divMinus data()[25] 3.205s passed
divMinusDenom data()[26] 3.191s passed
divLeastDPos data()[27] 3.161s passed
divLeastDNeg data()[28] 3.150s passed
divGreatestDPos data()[29] 3.154s passed
equivAllRight data()[2] 3.605s passed
divGreatestDNeg data()[30] 3.186s passed
divIncreasingPos data()[31] 3.148s passed
divIncreasingNeg data()[32] 3.146s passed
jdiv_zero data()[33] 3.124s passed
jdivPulloutMinusNum data()[34] 3.166s passed
jdivPulloutMinusDenom data()[35] 3.169s passed
jdiv_uniquePosPos data()[36] 3.139s passed
jdiv_uniquePosNeg data()[37] 3.168s passed
jdiv_uniqueNegPos data()[38] 3.178s passed
jdiv_uniqueNegNeg data()[39] 3.146s passed
irrflConcrete1 data()[3] 3.552s passed
jdivMultDenom1 data()[40] 3.165s passed
jdivMultDenom2 data()[41] 3.126s passed
mod_geZero data()[42] 3.156s passed
mod_lessDenom data()[43] 3.132s passed
jmod_NumPos data()[44] 3.135s passed
jmod_NumNeg data()[45] 3.156s passed
jmod_geZero data()[46] 3.149s passed
jmodNumZero data()[47] 3.155s passed
jmod_pulloutminusNum data()[48] 3.116s passed
jmod_pulloutminusDenom data()[49] 3.126s passed
irrflConcrete2 data()[4] 3.402s passed
jmodUnique1 data()[50] 3.219s passed
jmodUnique2 data()[51] 3.199s passed
intDivRem data()[52] 3.135s passed
jmodjmod data()[53] 3.146s passed
jmodDivisible data()[54] 3.167s passed
jmodDivisibleRep data()[55] 3.120s passed
jdivAddMultDenom data()[56] 3.274s passed
jmodAltZero data()[57] 3.173s passed
jmodAddMultDenomZero data()[58] 3.135s passed
polyDiv_zero data()[59] 3.138s passed
cancel_gtPos data()[5] 3.356s passed
polyMod_ltdivDenom data()[60] 3.138s passed
bsum_empty data()[61] 3.156s passed
bsum_induction_upper data()[62] 3.104s passed
bsum_induction_lower data()[63] 3.125s passed
bsum_num_of_bounds data()[64] 3.121s passed
bsum_num_of_bounds2 data()[65] 3.150s passed
bsum_induction_upper2 data()[66] 3.122s passed
bsum_induction_upper_concrete data()[67] 3.096s passed
bsum_induction_upper_concrete_2 data()[68] 3.091s passed
bsum_induction_upper2_concrete data()[69] 3.121s passed
cancel_gtNeg data()[6] 3.277s passed
bsum_induction_lower_concrete data()[70] 3.105s passed
bsum_induction_lower2 data()[71] 3.107s passed
bsum_induction_lower2_concrete data()[72] 3.109s passed
bsum_positive data()[73] 3.172s passed
bsum_upper_bound data()[74] 3.139s passed
bsum_lower_bound data()[75] 3.125s passed
bsum_positive_lower_bound_element data()[76] 3.172s passed
bsum_sub_same_index data()[77] 3.183s passed
bsum_less_same_index data()[78] 3.155s passed
bsum_equal_except_one_index data()[79] 3.137s passed
moduloIntIsInInt data()[7] 3.383s passed
bsum_num_of_is_max data()[80] 3.134s passed
bsum_num_of_is_max2 data()[81] 3.157s passed
bsum_num_of_is_max3 data()[82] 3.116s passed
bsum_num_of_is_max4 data()[83] 3.109s passed
bsum_num_of_lt_max data()[84] 3.111s passed
bsum_num_of_lt_max2 data()[85] 3.158s passed
bsum_num_of_lt_max3 data()[86] 3.134s passed
bsum_num_of_lt_max4 data()[87] 3.100s passed
bsum_num_of_gt0 data()[88] 3.107s passed
bsum_num_of_gt0_alt data()[89] 3.137s passed
moduloLongIsInLong data()[8] 3.244s passed
bsum_add_concrete data()[90] 3.106s passed
bprod_all_positive data()[91] 3.106s passed
bprod_split data()[92] 3.102s passed
powConcrete0 data()[93] 3.114s passed
powConcrete1 data()[94] 3.102s passed
powSplitFactor data()[95] 3.123s passed
powAdd data()[96] 3.115s passed
powMono data()[97] 3.152s passed
powMonoConcrete data()[98] 3.129s passed
powMonoConcreteRight data()[99] 3.119s passed
moduloShortIsInShort data()[9] 3.236s passed

Standard output

529        INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src/test/resources/testcase/dummyTrue.key 
549        DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 7.37ms 
753        INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
766        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)

1560       DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for Meta 
1561       DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for Meta 
1563       DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for Meta 
1563       DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for Meta 
3153       DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for JavaBigintExpression 
8627       DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 7.87s 
8690       INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof dummyTrue.key 
8724       DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 39.3ns 
8738       INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/firstOrder/Taclet_eqTermCut.proof 
8738       DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 625.8ns 
8743       INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
11549      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.81s 
11552      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: eqTermCut 
12547      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: eqTermCut 
12579      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 20.8ms 
12596      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/firstOrder/Taclet_equivAllRight.proof 
12596      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 518.8ns 
12601      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
15347      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.75s 
15348      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: equivAllRight 
16184      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: equivAllRight 
16198      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 9.66ms 
16201      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_irrflConcrete1.proof 
16202      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 423.3ns 
16204      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
18847      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.64s 
18847      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: irrflConcrete1 
19737      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: irrflConcrete1 
19749      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 5.8ms 
19755      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_irrflConcrete2.proof 
19755      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 157.1ns 
19757      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
22318      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.56s 
22318      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: irrflConcrete2 
23148      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: irrflConcrete2 
23154      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.34ms 
23157      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_cancel_gtPos.proof 
23158      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 438.7ns 
23159      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
25657      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.5s 
25658      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: cancel_gtPos 
26471      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: cancel_gtPos 
26510      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 35.05ms 
26514      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_cancel_gtNeg.proof 
26515      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 551ns 
26516      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
28991      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.47s 
28992      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: cancel_gtNeg 
29770      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: cancel_gtNeg 
29788      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 14.94ms 
29800      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intRulesIgnoringOF/Taclet_moduloIntIsInInt.proof 
29801      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 550.7ns 
29803      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
32365      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.56s 
32366      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: moduloIntIsInInt 
33169      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: moduloIntIsInInt 
33173      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 865.31ns 
33175      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intRulesIgnoringOF/Taclet_moduloLongIsInLong.proof 
33175      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 147.4ns 
33176      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
35621      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.45s 
35621      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: moduloLongIsInLong 
36414      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: moduloLongIsInLong 
36417      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 726.71ns 
36433      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intRulesIgnoringOF/Taclet_moduloShortIsInShort.proof 
36433      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 188.7ns 
36434      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
38868      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.43s 
38868      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: moduloShortIsInShort 
39664      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: moduloShortIsInShort 
39666      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 671ns 
39669      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intRulesIgnoringOF/Taclet_moduloByteIsInByte.proof 
39669      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 196.7ns 
39670      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
42099      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.43s 
42099      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: moduloByteIsInByte 
42868      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: moduloByteIsInByte 
42871      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 641.9ns 
42873      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intRulesIgnoringOF/Taclet_moduloCharIsInChar.proof 
42873      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 340.9ns 
42875      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
45296      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.42s 
45297      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: moduloCharIsInChar 
46087      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: moduloCharIsInChar 
46090      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 757.4ns 
46094      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_div_unique1.proof 
46095      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 441.2ns 
46097      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
48516      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.42s 
48516      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: div_unique1 
49301      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: div_unique1 
49340      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 34.47ms 
49342      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_div_unique2.proof 
49342      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 161ns 
49343      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
51729      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.39s 
51729      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: div_unique2 
52522      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: div_unique2 
52587      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 57.66ms 
52591      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_div_exists.proof 
52592      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 1.25ms 
52595      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
55025      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.43s 
55026      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: div_exists 
55790      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: div_exists 
55947      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 148.57ms 
55950      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_div_one.proof 
55950      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 161.1ns 
55951      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
58367      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.42s 
58368      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: div_one 
59154      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: div_one 
59159      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.49ms 
59161      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdiv_one.proof 
59161      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 284.9ns 
59163      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
61558      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.4s 
61559      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdiv_one 
62347      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdiv_one 
62351      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.2ms 
62355      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_div_zero.proof 
62355      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 385.6ns 
62356      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
64737      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.38s 
64738      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: div_zero 
65521      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: div_zero 
65558      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 32.47ms 
65561      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divResZero1.proof 
65561      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 376.5ns 
65563      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
67978      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.41s 
67979      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divResZero1 
68769      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divResZero1 
68797      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 23.39ms 
68801      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divResZero2.proof 
68801      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 397.3ns 
68804      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
71181      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.38s 
71182      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divResZero2 
71967      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divResZero2 
71979      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 8.69ms 
71982      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divResOne1.proof 
71982      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 424.2ns 
71984      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
74378      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.39s 
74378      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divResOne1 
75192      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divResOne1 
75215      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 18.87ms 
75229      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divResOne2.proof 
75229      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 172.6ns 
75230      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
77695      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.47s 
77696      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divResOne2 
78456      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divResOne2 
78469      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 10.43ms 
78482      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_div_cancel1.proof 
78482      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 398.5ns 
78483      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
80879      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.4s 
80880      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: div_cancel1 
81662      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: div_cancel1 
81683      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 16.54ms 
81685      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_div_cancel2.proof 
81685      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 143ns 
81686      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
84065      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.38s 
84066      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: div_cancel2 
84843      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: div_cancel2 
84847      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.47ms 
84848      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divAddMultDenom.proof 
84849      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 116.6ns 
84850      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
87235      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.39s 
87235      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divAddMultDenom 
88017      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divAddMultDenom 
88059      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 36.26ms 
88062      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divMinus.proof 
88063      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 359.9ns 
88064      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
90461      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.4s 
90462      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divMinus 
91216      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divMinus 
91265      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 42.22ms 
91268      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divMinusDenom.proof 
91268      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 370.7ns 
91270      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
93641      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.37s 
93642      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divMinusDenom 
94423      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divMinusDenom 
94457      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 27.61ms 
94461      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divLeastDPos.proof 
94463      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 1.58ms 
94464      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
96834      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.37s 
96835      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divLeastDPos 
97611      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divLeastDPos 
97618      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 5.2ms 
97620      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divLeastDNeg.proof 
97620      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 106.4ns 
97621      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
99979      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.36s 
99979      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divLeastDNeg 
100756     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divLeastDNeg 
100768     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 9.74ms 
100770     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divGreatestDPos.proof 
100770     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 116.6ns 
100771     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
103156     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.39s 
103157     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divGreatestDPos 
103911     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divGreatestDPos 
103922     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 8.22ms 
103923     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divGreatestDNeg.proof 
103924     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 123.5ns 
103924     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
106319     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.39s 
106320     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divGreatestDNeg 
107101     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divGreatestDNeg 
107108     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 5.23ms 
107110     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divIncreasingPos.proof 
107110     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 114.5ns 
107111     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
109473     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.36s 
109473     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divIncreasingPos 
110248     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divIncreasingPos 
110256     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 5.01ms 
110258     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divIncreasingNeg.proof 
110258     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 132.7ns 
110259     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
112613     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.35s 
112613     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divIncreasingNeg 
113396     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divIncreasingNeg 
113403     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.45ms 
113404     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdiv_zero.proof 
113404     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 125.3ns 
113405     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
115773     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.37s 
115773     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdiv_zero 
116522     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdiv_zero 
116526     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.63ms 
116527     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdivPulloutMinusNum.proof 
116528     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 94.1ns 
116528     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
118905     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.38s 
118905     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdivPulloutMinusNum 
119681     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdivPulloutMinusNum 
119692     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 8.92ms 
119694     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdivPulloutMinusDenom.proof 
119694     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 123ns 
119695     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
122050     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.35s 
122050     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdivPulloutMinusDenom 
122827     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdivPulloutMinusDenom 
122860     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 28.11ms 
122863     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdiv_uniquePosPos.proof 
122864     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 333.6ns 
122865     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
125207     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.34s 
125208     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdiv_uniquePosPos 
125983     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdiv_uniquePosPos 
125999     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 12.19ms 
126002     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdiv_uniquePosNeg.proof 
126002     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 325ns 
126003     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
128375     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.37s 
128376     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdiv_uniquePosNeg 
129145     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdiv_uniquePosNeg 
129167     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 14.75ms 
129170     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdiv_uniqueNegPos.proof 
129170     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 329.8ns 
129171     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
131557     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.39s 
131557     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdiv_uniqueNegPos 
132332     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdiv_uniqueNegPos 
132346     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 11.17ms 
132348     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdiv_uniqueNegNeg.proof 
132348     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 109.9ns 
132349     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
134707     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.36s 
134707     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdiv_uniqueNegNeg 
135479     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdiv_uniqueNegNeg 
135492     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 10.21ms 
135493     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdivMultDenom1.proof 
135493     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 119.1ns 
135494     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
137848     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.35s 
137848     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdivMultDenom1 
138628     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdivMultDenom1 
138657     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 24.44ms 
138659     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdivMultDenom2.proof 
138659     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 110.1ns 
138660     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
141028     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.37s 
141028     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdivMultDenom2 
141781     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdivMultDenom2 
141784     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.11ms 
141785     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_mod_geZero.proof 
141785     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 85.7ns 
141786     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
144161     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.37s 
144161     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: mod_geZero 
144935     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: mod_geZero 
144939     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2ms 
144941     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_mod_lessDenom.proof 
144941     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 105.1ns 
144942     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
147291     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.35s 
147291     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: mod_lessDenom 
148065     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: mod_lessDenom 
148072     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.77ms 
148073     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmod_NumPos.proof 
148073     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 103ns 
148074     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
150424     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.35s 
150424     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmod_NumPos 
151199     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmod_NumPos 
151206     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 5.14ms 
151208     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmod_NumNeg.proof 
151208     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 101.5ns 
151209     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
153576     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.37s 
153576     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmod_NumNeg 
154329     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmod_NumNeg 
154357     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 25.24ms 
154368     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmod_geZero.proof 
154369     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 360.5ns 
154370     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
156736     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.37s 
156737     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmod_geZero 
157508     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmod_geZero 
157516     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 5.59ms 
157517     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmodNumZero.proof 
157517     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 80.4ns 
157518     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
159888     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.37s 
159888     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmodNumZero 
160667     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmodNumZero 
160670     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.12ms 
160672     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmod_pulloutminusNum.proof 
160673     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 279.4ns 
160674     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
163011     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.34s 
163012     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmod_pulloutminusNum 
163783     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmod_pulloutminusNum 
163787     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.35ms 
163788     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmod_pulloutminusDenom.proof 
163788     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 96.1ns 
163789     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
166158     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.37s 
166158     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmod_pulloutminusDenom 
166909     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmod_pulloutminusDenom 
166912     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.72ms 
166914     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmodUnique1.proof 
166914     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 104.2ns 
166915     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
169293     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.38s 
169294     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmodUnique1 
170070     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmodUnique1 
170130     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 51.47ms 
170134     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmodUnique2.proof 
170134     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 311.3ns 
170135     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
172489     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.35s 
172490     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmodUnique2 
173268     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmodUnique2 
173331     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 53.21ms 
173332     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_intDivRem.proof 
173333     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 117.6ns 
173333     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
175692     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.36s 
175692     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: intDivRem 
176463     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: intDivRem 
176467     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.32ms 
176468     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmodjmod.proof 
176468     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 89.8ns 
176469     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
178836     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.37s 
178836     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmodjmod 
179584     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmodjmod 
179612     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 23.82ms 
179613     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmodDivisible.proof 
179614     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 244.7ns 
179614     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
181986     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.37s 
181986     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmodDivisible 
182759     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmodDivisible 
182779     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 17.1ms 
182781     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmodDivisibleRep.proof 
182781     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 116.9ns 
182782     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
185125     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.34s 
185125     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmodDivisibleRep 
185897     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmodDivisibleRep 
185899     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.01ms 
185901     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdivAddMultDenom.proof 
185901     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 78.3ns 
185902     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
188267     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.36s 
188268     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdivAddMultDenom 
189066     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdivAddMultDenom 
189173     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 90.73ms 
189175     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmodAltZero.proof 
189175     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 109.2ns 
189176     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
191559     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.38s 
191559     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmodAltZero 
192338     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmodAltZero 
192347     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 6.28ms 
192348     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmodAddMultDenomZero.proof 
192348     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 95.4ns 
192349     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
194706     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.36s 
194707     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmodAddMultDenomZero 
195475     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmodAddMultDenomZero 
195481     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.05ms 
195482     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_polyDiv_zero.proof 
195482     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 83.4ns 
195483     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
197832     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.35s 
197833     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: polyDiv_zero 
198604     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: polyDiv_zero 
198619     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 12.23ms 
198621     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_polyMod_ltdivDenom.proof 
198621     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 103.8ns 
198621     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
200994     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.37s 
200995     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: polyMod_ltdivDenom 
201745     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: polyMod_ltdivDenom 
201756     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.45ms 
201759     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_empty.proof 
201759     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 96.1ns 
201760     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
204140     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.38s 
204141     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_empty 
204909     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_empty 
204913     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.48ms 
204914     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_induction_upper.proof 
204914     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 67.6ns 
204915     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
207245     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.33s 
207246     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_upper 
208014     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_induction_upper 
208017     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.06ms 
208019     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_induction_lower.proof 
208019     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 73.8ns 
208020     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
210358     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.34s 
210358     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_lower 
211127     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_induction_lower 
211142     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 11.77ms 
211144     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_bounds.proof 
211144     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 90.9ns 
211145     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
213480     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.33s 
213480     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_bounds 
214251     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_bounds 
214264     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 9.58ms 
214265     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_bounds2.proof 
214265     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 91.8ns 
214266     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
216625     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.36s 
216625     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_bounds2 
217402     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_bounds2 
217414     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 8.91ms 
217415     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_induction_upper2.proof 
217415     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 87.8ns 
217416     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
219758     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.34s 
219758     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_upper2 
220532     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_induction_upper2 
220535     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.11ms 
220537     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_induction_upper_concrete.proof 
220537     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 82.7ns 
220538     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
222863     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.32s 
222863     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_upper_concrete 
223628     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_induction_upper_concrete 
223632     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.33ms 
223633     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_induction_upper_concrete_2.proof 
223633     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 79.3ns 
223634     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
225975     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.34s 
225975     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_upper_concrete_2 
226718     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_induction_upper_concrete_2 
226722     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.64ms 
226724     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_induction_upper2_concrete.proof 
226724     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 82.2ns 
226724     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
229073     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.35s 
229073     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_upper2_concrete 
229841     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_induction_upper2_concrete 
229843     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 877.51ns 
229844     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_induction_lower_concrete.proof 
229845     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 83.1ns 
229845     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
232178     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.33s 
232178     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_lower_concrete 
232946     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_induction_lower_concrete 
232949     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 535.7ns 
232950     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_induction_lower2.proof 
232950     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 73.7ns 
232951     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
235280     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.33s 
235280     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_lower2 
236052     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_induction_lower2 
236056     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.71ms 
236057     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_induction_lower2_concrete.proof 
236057     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 81.5ns 
236058     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
238414     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.36s 
238414     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_lower2_concrete 
239162     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_induction_lower2_concrete 
239164     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 791.1ns 
239166     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_positive.proof 
239166     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 62.2ns 
239166     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
241525     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.36s 
241525     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_positive 
242302     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_positive 
242336     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 31.39ms 
242338     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_upper_bound.proof 
242338     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 97.8ns 
242339     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
244680     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.34s 
244681     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_upper_bound 
245448     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_upper_bound 
245475     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 23.12ms 
245477     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_lower_bound.proof 
245477     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 234.7ns 
245478     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
247810     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.33s 
247810     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_lower_bound 
248578     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_lower_bound 
248601     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 19.13ms 
248602     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_positive_lower_bound_element.proof 
248602     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 78.9ns 
248603     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
250990     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.39s 
250991     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_positive_lower_bound_element 
251741     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_positive_lower_bound_element 
251772     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 26.83ms 
251774     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_sub_same_index.proof 
251774     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 77.5ns 
251775     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
254159     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.38s 
254160     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_sub_same_index 
254929     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_sub_same_index 
254955     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 22.89ms 
254958     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_less_same_index.proof 
254958     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 240.92ns 
254959     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
257308     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.35s 
257308     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_less_same_index 
258073     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_less_same_index 
258110     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 32.33ms 
258112     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_equal_except_one_index.proof 
258112     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 76.7ns 
258113     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
260458     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.35s 
260459     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_equal_except_one_index 
261228     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_equal_except_one_index 
261247     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 15.61ms 
261249     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_is_max.proof 
261249     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 81.41ns 
261250     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
263622     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.37s 
263622     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_is_max 
264367     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_is_max 
264381     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 11.64ms 
264383     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_is_max2.proof 
264383     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 91.8ns 
264384     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
266753     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.37s 
266753     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_is_max2 
267521     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_is_max2 
267537     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 13.18ms 
267540     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_is_max3.proof 
267541     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 231.1ns 
267542     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
269874     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.33s 
269874     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_is_max3 
270642     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_is_max3 
270655     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 10.28ms 
270656     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_is_max4.proof 
270657     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 69.3ns 
270657     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
272980     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.32s 
272980     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_is_max4 
273747     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_is_max4 
273764     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 14.36ms 
273766     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_lt_max.proof 
273766     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 87.2ns 
273767     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
276112     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.34s 
276112     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_lt_max 
276858     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_lt_max 
276876     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 14.23ms 
276877     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_lt_max2.proof 
276877     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 90.8ns 
276878     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
279240     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.36s 
279240     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_lt_max2 
280010     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_lt_max2 
280032     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 17.58ms 
280035     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_lt_max3.proof 
280035     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 223.11ns 
280038     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
282384     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.35s 
282385     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_lt_max3 
283152     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_lt_max3 
283168     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 12.69ms 
283169     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_lt_max4.proof 
283169     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 91.1ns 
283170     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
285487     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.32s 
285488     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_lt_max4 
286253     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_lt_max4 
286267     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 11.37ms 
286269     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_gt0.proof 
286269     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 74.5ns 
286269     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
288614     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.34s 
288614     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_gt0 
289358     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_gt0 
289374     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 12.64ms 
289375     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_gt0_alt.proof 
289375     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 84.8ns 
289376     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
291720     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.34s 
291721     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_gt0_alt 
292495     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_gt0_alt 
292511     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 13.79ms 
292513     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_add_concrete.proof 
292513     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 81.3ns 
292513     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
294844     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.33s 
294844     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_add_concrete 
295612     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_add_concrete 
295618     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.89ms 
295619     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bprod/Taclet_bprod_all_positive.proof 
295619     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 68.6ns 
295620     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
297936     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.32s 
297936     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bprod_all_positive 
298709     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bprod_all_positive 
298723     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 10.44ms 
298726     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bprod/Taclet_bprod_split.proof 
298726     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 214.4ns 
298727     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
301078     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.35s 
301078     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bprod_split 
301822     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bprod_split 
301826     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.67ms 
301827     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powConcrete0.proof 
301827     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 74.2ns 
301828     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
304170     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.34s 
304171     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powConcrete0 
304938     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powConcrete0 
304940     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 627.31ns 
304941     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powConcrete1.proof 
304942     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 69.5ns 
304942     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
307273     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.33s 
307273     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powConcrete1 
308040     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powConcrete1 
308043     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 665.71ns 
308044     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powSplitFactor.proof 
308044     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 57ns 
308045     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
310377     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.33s 
310377     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powSplitFactor 
311152     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powSplitFactor 
311165     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.24ms 
311166     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powAdd.proof 
311166     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 78.8ns 
311167     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
313525     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.36s 
313525     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powAdd 
314275     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powAdd 
314281     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.28ms 
314282     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powMono.proof 
314282     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 62.6ns 
314283     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
316650     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.37s 
316650     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powMono 
317422     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powMono 
317432     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 7.78ms 
317434     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powMonoConcrete.proof 
317434     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 69.4ns 
317434     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
319784     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.35s 
319785     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powMonoConcrete 
320557     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powMonoConcrete 
320561     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.94ms 
320562     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powMonoConcreteRight.proof 
320562     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 60.8ns 
320563     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
322904     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.34s 
322905     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powMonoConcreteRight 
323679     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powMonoConcreteRight 
323681     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 475.51ns 
323682     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powPositive.proof 
323682     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 70.1ns 
323683     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
326053     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.37s 
326053     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powPositive 
326803     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powPositive 
326808     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.02ms 
326810     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powPositiveConcrete.proof 
326810     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 89.9ns 
326810     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
329171     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.36s 
329171     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powPositiveConcrete 
329942     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powPositiveConcrete 
329944     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 538.71ns 
329945     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powGeq1Concrete.proof 
329945     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 62.8ns 
329946     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
332293     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.35s 
332293     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powGeq1Concrete 
333071     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powGeq1Concrete 
333073     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 514.6ns 
333074     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_pow2InIntLower.proof 
333074     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 70.6ns 
333075     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
335415     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.34s 
335415     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: pow2InIntLower 
336184     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: pow2InIntLower 
336186     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 526.41ns 
336187     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_pow2InIntUpper.proof 
336187     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 71.1ns 
336188     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
338540     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.35s 
338540     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: pow2InIntUpper 
339285     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: pow2InIntUpper 
339289     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.99ms 
339290     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logSelfConcrete.proof 
339290     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 59.5ns 
339291     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
341654     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.36s 
341655     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logSelfConcrete 
342427     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logSelfConcrete 
342434     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.84ms 
342437     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_log1Concrete.proof 
342437     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 211.5ns 
342438     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
344775     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.34s 
344775     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: log1Concrete 
345545     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: log1Concrete 
345549     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.65ms 
345550     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logProduct.proof 
345550     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 74.1ns 
345551     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
347883     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.33s 
347883     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logProduct 
348653     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logProduct 
348659     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.59ms 
348661     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logTimesBaseConcrete.proof 
348661     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 74.9ns 
348661     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
351008     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.35s 
351008     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logTimesBaseConcrete 
351753     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logTimesBaseConcrete 
351757     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.17ms 
351759     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logProdIdentity.proof 
351759     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 99.4ns 
351759     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
354136     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.38s 
354136     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logProdIdentity 
354908     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logProdIdentity 
354922     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 10.5ms 
354923     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logProdIdentityConcrete.proof 
354923     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 80.3ns 
354924     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
357279     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.35s 
357279     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logProdIdentityConcrete 
358052     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logProdIdentityConcrete 
358055     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.67ms 
358057     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logPowIdentity.proof 
358057     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 101.2ns 
358058     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
360402     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.34s 
360402     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logPowIdentity 
361174     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logPowIdentity 
361177     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.14ms 
361179     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logPowIdentityConcrete.proof 
361179     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 57.4ns 
361180     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
363555     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.38s 
363556     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logPowIdentityConcrete 
364304     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logPowIdentityConcrete 
364308     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.71ms 
364309     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logPositive.proof 
364309     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 68ns 
364310     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
366680     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.37s 
366681     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logPositive 
367453     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logPositive 
367467     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 11.19ms 
367468     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logPositiveConcrete.proof 
367468     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 74.6ns 
367469     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
369821     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.35s 
369821     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logPositiveConcrete 
370593     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logPositiveConcrete 
370597     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 361.5ns 
370600     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logMono.proof 
370600     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 68.3ns 
370601     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
372957     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.36s 
372957     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logMono 
373704     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logMono 
373731     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 22.49ms 
373733     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logMonoConcrete.proof 
373733     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 68.1ns 
373733     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
376097     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.36s 
376098     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logMonoConcrete 
376865     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logMonoConcrete 
376869     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.85ms 
376870     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powLogLess.proof 
376870     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 62.2ns 
376871     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
379214     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.34s 
379214     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powLogLess 
379990     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powLogLess 
380007     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 12.64ms 
380009     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powLogMore2.proof 
380010     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 227.9ns 
380010     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
382367     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.36s 
382367     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powLogMore2 
383117     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powLogMore2 
383131     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 11.55ms 
383133     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logLessThanPow.proof 
383133     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 77ns 
383133     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
385493     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.36s 
385493     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logLessThanPow 
386260     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logLessThanPow 
386278     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 14.59ms 
386279     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logLessThanPowConcrete.proof 
386280     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 85.6ns 
386280     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
388616     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.34s 
388616     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logLessThanPowConcrete 
389386     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logLessThanPowConcrete 
389389     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 557.31ns 
389390     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logSqueeze.proof 
389390     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 58.2ns 
389391     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
391747     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.36s 
391747     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logSqueeze 
392491     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logSqueeze 
392496     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.26ms 
392498     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/booleanRules/Taclet_ifthenelse_equals.proof 
392498     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 64.1ns 
392498     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
394847     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.35s 
394847     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: ifthenelse_equals 
395619     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: ifthenelse_equals 
395622     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.37ms 
395623     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/booleanRules/Taclet_ifthenelse_equals_1.proof 
395623     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 69.8ns 
395624     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
397966     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.34s 
397966     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: ifthenelse_equals_1 
398746     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: ifthenelse_equals_1 
398749     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 798.41ns 
398750     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/booleanRules/Taclet_ifthenelse_equals_2.proof 
398750     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 61.1ns 
398751     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
401101     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.35s 
401101     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: ifthenelse_equals_2 
401853     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: ifthenelse_equals_2 
401856     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 822.11ns 
401857     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/locSet/Taclet_disjointWithSingleton1.proof 
401857     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 69ns 
401858     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
404214     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.36s 
404214     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: disjointWithSingleton1 
404991     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: disjointWithSingleton1 
404994     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.3ms 
404995     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/locSet/Taclet_disjointWithSingleton2.proof 
404995     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 58ns 
404996     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
407354     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.36s 
407354     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: disjointWithSingleton2 
408108     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: disjointWithSingleton2 
408110     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.17ms 
408112     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/locSet/Taclet_disjointArrayRanges.proof 
408112     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 71.8ns 
408113     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
410475     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.36s 
410475     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: disjointArrayRanges 
411253     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: disjointArrayRanges 
411261     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 5.55ms 
411263     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/locSet/Taclet_disjointArrayRangeAllFields1.proof 
411263     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 61ns 
411264     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
413614     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.35s 
413614     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: disjointArrayRangeAllFields1 
414396     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: disjointArrayRangeAllFields1 
414403     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 5.14ms 
414404     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/locSet/Taclet_disjointArrayRangeAllFields2.proof 
414404     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 81.2ns 
414405     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
416758     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.35s 
416759     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: disjointArrayRangeAllFields2 
417534     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: disjointArrayRangeAllFields2 
417540     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.33ms 
417542     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqSelfDefinition.proof 
417542     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 58.2ns 
417543     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
419881     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.34s 
419881     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqSelfDefinition 
420663     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqSelfDefinition 
420671     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 5.54ms 
420672     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqOutsideValue.proof 
420672     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 124.1ns 
420673     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
423025     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.35s 
423025     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqOutsideValue 
423811     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqOutsideValue 
423815     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.27ms 
423817     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_castedGetAny.proof 
423817     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 77.1ns 
423817     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
426165     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.35s 
426165     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: castedGetAny 
426950     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: castedGetAny 
426956     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.43ms 
426957     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqGetAlphaCast.proof 
426957     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 63.9ns 
426958     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
429326     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.37s 
429326     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqGetAlphaCast 
430091     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqGetAlphaCast 
430093     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 742.72ns 
430095     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqSingleton.proof 
430095     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 63.3ns 
430095     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
432455     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.36s 
432456     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqSingleton 
433238     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqSingleton 
433241     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.05ms 
433242     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqSingletonConcrete.proof 
433242     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 78.5ns 
433243     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
435596     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.35s 
435596     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqSingletonConcrete 
436353     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqSingletonConcrete 
436355     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 877.57ns 
436358     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqConcat.proof 
436358     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 67.31ns 
436359     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
438708     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.35s 
438709     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqConcat 
439487     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqConcat 
439495     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 6.26ms 
439496     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqSub.proof 
439496     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 71.1ns 
439497     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
441850     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.35s 
441850     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqSub 
442632     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqSub 
442635     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.1ms 
442636     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqReverse.proof 
442636     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 69.2ns 
442637     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
444974     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.34s 
444974     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqReverse 
445758     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqReverse 
445763     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.57ms 
445765     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqEmpty.proof 
445765     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 69.3ns 
445765     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
448138     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.37s 
448138     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqEmpty 
448929     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqEmpty 
448931     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 882.12ns 
448932     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqSingleton.proof 
448932     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 66ns 
448933     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
451282     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.35s 
451282     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqSingleton 
452064     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqSingleton 
452066     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 647.22ns 
452067     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqConcat.proof 
452067     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 56.1ns 
452068     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
454430     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.36s 
454430     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqConcat 
455213     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqConcat 
455216     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.36ms 
455218     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqSub.proof 
455218     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 70.4ns 
455218     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
457589     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.37s 
457589     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqSub 
458351     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqSub 
458353     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 770.72ns 
458355     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqReverse.proof 
458355     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 54.2ns 
458355     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
460728     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.37s 
460728     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqReverse 
461515     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqReverse 
461518     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.06ms 
461519     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_equalityToSeqGetAndSeqLenLeft.proof 
461519     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 58.6ns 
461520     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
463891     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.37s 
463891     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: equalityToSeqGetAndSeqLenLeft 
464677     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: equalityToSeqGetAndSeqLenLeft 
464680     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 963.22ns 
464681     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_equalityToSeqGetAndSeqLenRight.proof 
464681     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 67.1ns 
464682     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
467034     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.35s 
467034     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: equalityToSeqGetAndSeqLenRight 
467825     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: equalityToSeqGetAndSeqLenRight 
467828     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.11ms 
467830     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqSingletonEQ.proof 
467830     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 63.5ns 
467831     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
470196     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.37s 
470196     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqSingletonEQ 
470977     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqSingletonEQ 
470980     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 859.52ns 
470981     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqConcatEQ.proof 
470981     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 74.6ns 
470982     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
473346     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.36s 
473346     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqConcatEQ 
474112     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqConcatEQ 
474121     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 6.73ms 
474122     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqSubEQ.proof 
474122     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 79.9ns 
474123     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
476487     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.36s 
476487     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqSubEQ 
477272     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqSubEQ 
477274     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 615.11ns 
477276     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqReverseEQ.proof 
477276     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 77.7ns 
477277     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
479655     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.38s 
479656     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqReverseEQ 
480440     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqReverseEQ 
480446     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.82ms 
480447     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqEmptyEQ.proof 
480447     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 78.9ns 
480448     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
482809     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.36s 
482809     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqEmptyEQ 
483571     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqEmptyEQ 
483574     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 929.02ns 
483575     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqSingletonEQ.proof 
483575     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 69.1ns 
483576     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
485923     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.35s 
485923     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqSingletonEQ 
486704     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqSingletonEQ 
486706     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 702.31ns 
486708     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqConcatEQ.proof 
486708     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 94.8ns 
486709     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
489067     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.36s 
489067     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqConcatEQ 
489850     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqConcatEQ 
489854     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.82ms 
489856     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqSubEQ.proof 
489856     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 211.31ns 
489857     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
492216     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.36s 
492216     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqSubEQ 
492999     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqSubEQ 
493002     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 969.51ns 
493004     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqReverseEQ.proof 
493004     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 212.2ns 
493005     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
495344     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.34s 
495344     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqReverseEQ 
496129     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqReverseEQ 
496132     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.18ms 
496133     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqDefEQ.proof 
496133     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 65.7ns 
496134     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
498485     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.35s 
498485     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqDefEQ 
499270     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqDefEQ 
499273     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.05ms 
499274     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqDefEQ.proof 
499274     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 53.6ns 
499275     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
501640     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.37s 
501640     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqDefEQ 
502426     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqDefEQ 
502430     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.02ms 
502431     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqConcatWithSeqEmpty1.proof 
502431     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 65.9ns 
502432     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
504792     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.36s 
504792     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqConcatWithSeqEmpty1 
505577     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqConcatWithSeqEmpty1 
505584     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 5.34ms 
505585     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqConcatWithSeqEmpty2.proof 
505586     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 82.9ns 
505586     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
507941     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.35s 
507941     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqConcatWithSeqEmpty2 
508725     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqConcatWithSeqEmpty2 
508733     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 5.65ms 
508734     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqReverseOfSeqEmpty.proof 
508735     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 74.7ns 
508735     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
511093     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.36s 
511093     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqReverseOfSeqEmpty 
511876     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqReverseOfSeqEmpty 
511882     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.35ms 
511884     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_subSeqComplete.proof 
511884     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 70.3ns 
511885     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
514244     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.36s 
514244     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: subSeqComplete 
515028     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: subSeqComplete 
515034     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.21ms 
515035     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_subSeqTailR.proof 
515036     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 78ns 
515036     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
517391     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.35s 
517391     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: subSeqTailR 
518172     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: subSeqTailR 
518182     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 7.34ms 
518183     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_subSeqTailL.proof 
518183     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 72.7ns 
518184     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
520542     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.36s 
520542     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: subSeqTailL 
521326     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: subSeqTailL 
521336     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 7.45ms 
521338     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_subSeqTailEQR.proof 
521338     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 76.4ns 
521339     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
523709     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.37s 
523709     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: subSeqTailEQR 
524471     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: subSeqTailEQR 
524480     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 6.93ms 
524482     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_subSeqTailEQL.proof 
524482     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 64.8ns 
524482     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
526833     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.35s 
526833     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: subSeqTailEQL 
527618     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: subSeqTailEQL 
527625     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.76ms 
527627     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDef_split.proof 
527627     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 65.4ns 
527627     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
529975     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.35s 
529975     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_split 
530757     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDef_split 
530776     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 15.65ms 
530778     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDef_induction_upper.proof 
530778     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 63.8ns 
530779     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
533133     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.35s 
533133     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_induction_upper 
533919     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDef_induction_upper 
533940     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 17.31ms 
533942     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDef_induction_upper_concrete.proof 
533942     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 78.6ns 
533943     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
536302     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.36s 
536302     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_induction_upper_concrete 
537086     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDef_induction_upper_concrete 
537105     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 15.2ms 
537106     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDef_induction_lower.proof 
537106     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 72.2ns 
537107     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
539461     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.35s 
539461     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_induction_lower 
540245     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDef_induction_lower 
540263     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 14.24ms 
540264     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDef_induction_lower_concrete.proof 
540264     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 76.7ns 
540265     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
542616     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.35s 
542616     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_induction_lower_concrete 
543401     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDef_induction_lower_concrete 
543419     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 14.79ms 
543421     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDef_split_in_three.proof 
543421     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 68.8ns 
543422     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
545783     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.36s 
545784     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_split_in_three 
546564     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDef_split_in_three 
546609     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 37.53ms 
546610     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDef_empty.proof 
546610     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 77ns 
546611     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
548959     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.35s 
548959     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_empty 
549744     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDef_empty 
549753     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.93ms 
549756     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDef_one_summand.proof 
549756     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 237.8ns 
549757     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
552133     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.38s 
552134     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_one_summand 
552921     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDef_one_summand 
552926     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3ms 
552927     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDef_lower_equals_upper.proof 
552927     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 75.2ns 
552928     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
555286     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.36s 
555287     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_lower_equals_upper 
556072     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDef_lower_equals_upper 
556076     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.9ms 
556077     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDefOfSeq.proof 
556077     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 59.4ns 
556078     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
558445     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.37s 
558445     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDefOfSeq 
559230     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDefOfSeq 
559243     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 9.47ms 
559244     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqSelfDefinitionEQ2.proof 
559244     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 77.3ns 
559245     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
561609     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.36s 
561609     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqSelfDefinitionEQ2 
562397     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqSelfDefinitionEQ2 
562403     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.96ms 
562405     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_indexOfSeqSingleton.proof 
562405     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 74.5ns 
562406     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
564775     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.37s 
564775     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: indexOfSeqSingleton 
565558     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: indexOfSeqSingleton 
565561     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.31ms 
565563     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_indexOfSeqConcatFirst.proof 
565563     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 71ns 
565564     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
567924     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.36s 
567924     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: indexOfSeqConcatFirst 
568710     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: indexOfSeqConcatFirst 
568720     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 7.46ms 
568721     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_indexOfSeqConcatSecond.proof 
568721     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 82.5ns 
568722     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
571089     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.37s 
571090     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: indexOfSeqConcatSecond 
571875     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: indexOfSeqConcatSecond 
571885     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 7.73ms 
571886     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_indexOfSeqSub.proof 
571886     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 71.7ns 
571887     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
574245     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.36s 
574245     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: indexOfSeqSub 
575027     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: indexOfSeqSub 
575041     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 10.14ms 
575043     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfArray2seq.proof 
575043     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 226.2ns 
575044     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
577403     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.36s 
577403     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfArray2seq 
578192     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfArray2seq 
578195     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.05ms 
578196     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getAnyOfArray2seq.proof 
578196     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 73ns 
578197     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
580558     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.36s 
580558     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getAnyOfArray2seq 
581344     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getAnyOfArray2seq 
581348     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.65ms 
581349     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfArray2seq.proof 
581349     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 60.3ns 
581350     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
583707     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.36s 
583707     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfArray2seq 
584497     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfArray2seq 
584503     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.1ms 
584504     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_getAnyOfNPermInv.proof 
584504     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 77.7ns 
584505     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
586878     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.37s 
586878     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getAnyOfNPermInv 
587666     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getAnyOfNPermInv 
587670     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.54ms 
587672     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqNPermRange.proof 
587672     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 79.1ns 
587672     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
590028     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.36s 
590029     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqNPermRange 
590821     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqNPermRange 
590862     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 35.49ms 
590864     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermTrans.proof 
590864     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 85.9ns 
590865     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
593258     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.39s 
593258     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermTrans 
594041     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermTrans 
594058     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 13.92ms 
594060     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermRefl.proof 
594060     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 96.3ns 
594061     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
596413     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.35s 
596413     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermRefl 
597196     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermRefl 
597207     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 8.49ms 
597209     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermSplit.proof 
597209     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 77.5ns 
597209     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
599563     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.35s 
599563     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermSplit 
600346     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermSplit 
600348     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 185.6ns 
600349     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqNPermRight.proof 
600349     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 58.4ns 
600350     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
602719     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.37s 
602719     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqNPermRight 
603507     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqNPermRight 
603587     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 69.06ms 
603589     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermFromSwap.proof 
603589     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 68.4ns 
603590     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
605950     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.36s 
605950     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermFromSwap 
606734     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermFromSwap 
606767     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 28.68ms 
606769     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermTransAlt0.proof 
606769     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 71.6ns 
606770     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
609154     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.38s 
609154     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermTransAlt0 
609939     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermTransAlt0 
609941     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 285.4ns 
609943     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermTransAlt1.proof 
609943     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 59.1ns 
609943     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
612289     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.35s 
612289     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermTransAlt1 
613070     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermTransAlt1 
613071     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 219.8ns 
613073     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermTransAlt2.proof 
613073     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 67.1ns 
613074     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
615410     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.34s 
615410     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermTransAlt2 
616189     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermTransAlt2 
616191     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 228.2ns 
616193     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermTransAlt3.proof 
616193     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 59.7ns 
616193     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
618526     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.33s 
618526     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermTransAlt3 
619305     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermTransAlt3 
619307     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 346.5ns 
619308     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermForall.proof 
619309     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 68.4ns 
619309     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
621672     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.36s 
621672     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermForall 
622453     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermForall 
622532     INFO  Test worker     d.u.i.k.s.SMTFocusResults Analyzing unsat core: (L_1 L_3 L_4) 
622539     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 83.65ms 
622548     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermExists.proof 
622548     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 243.5ns 
622549     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
624900     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.35s 
624900     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermExists 
625682     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermExists 
625724     INFO  Test worker     d.u.i.k.s.SMTFocusResults Analyzing unsat core: (L_1 L_3 L_5 L_6 L_7) 
625725     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 40.98ms 
625727     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm2/Taclet_schiffl_lemma_2.proof 
625727     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 73.8ns 
625729     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
628073     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.34s 
628073     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: schiffl_lemma_2 
628878     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: schiffl_lemma_2 
628880     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.2ns 
628910     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [1] goal: 0, source line: 49, command: 'macro split-prop' 
628963     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [2] goal: 3, source line: 50, command: 'rule allRight' 
628981     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [3] goal: 4, source line: 51, command: 'rule allRight' 
628988     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [4] goal: 5, source line: 52, command: 'macro split-prop' 
629004     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [5] goal: 11, source line: 53, command: 'rule 'seqPermDefLeft'' 
629005     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [6] goal: 12, source line: 54, command: 'rule 'andLeft'' 
629007     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [7] goal: 13, source line: 55, command: 'rule 'exLeft'' 
629009     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [8] goal: 14, source line: 56, command: 'macro split-prop' 
629014     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [9] goal: 16, source line: 57, command: 'rule  seqNPermRange' 
629016     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' 
629018     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [11] goal: 18, source line: 60, command: 'rule impLeft' 
629019     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [12] goal: 19, source line: 61, command: 'tryclose branch' 
629244     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [13] goal: 20, source line: 62, command: 'rule andLeft' 
629246     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [14] goal: 97, source line: 63, command: 'rule andLeft' 
629249     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' 
629249     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [16] goal: 99, source line: 66, command: 'rule impLeft' 
629251     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [17] goal: 100, source line: 67, command: 'tryclose branch' 
629376     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [18] goal: 101, source line: 68, command: 'rule andLeft' 
629377     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [19] goal: 188, source line: 69, command: 'rule andLeft' 
629381     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [20] goal: 189, source line: 70, command: 'rule seqNPermDefLeft' 
629382     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' 
629383     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [22] goal: 191, source line: 73, command: 'rule impLeft' 
629385     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [23] goal: 192, source line: 74, command: 'tryclose branch' 
629537     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [24] goal: 193, source line: 75, command: 'rule exLeft' 
629540     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [25] goal: 310, source line: 76, command: 'rule andLeft' 
629541     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [26] goal: 311, source line: 77, command: 'rule andLeft' 
629542     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' 
629542     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [28] goal: 313, source line: 80, command: 'rule impLeft' 
629545     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [29] goal: 314, source line: 81, command: 'tryclose branch' 
629685     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [30] goal: 315, source line: 82, command: 'rule exLeft' 
629687     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [31] goal: 420, source line: 83, command: 'rule andLeft' 
629688     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [32] goal: 421, source line: 84, command: 'rule andLeft' 
629689     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' 
629690     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [34] goal: 423, source line: 87, command: 'rule impLeft' 
629691     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [35] goal: 424, source line: 88, command: 'tryclose branch' 
629698     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [36] goal: 425, source line: 89, command: 'rule andLeft' 
629698     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [37] goal: 434, source line: 90, command: 'rule andLeft' 
629702     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' 
629703     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' 
629705     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [40] goal: 437, source line: 94, command: 'rule impLeft' 
629706     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [41] goal: 438, source line: 95, command: 'tryclose branch' 
629714     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [42] goal: 439, source line: 96, command: 'rule andLeft' 
629714     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [43] goal: 448, source line: 97, command: 'rule andLeft' 
629715     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' 
629716     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [45] goal: 450, source line: 99, command: 'instantiate var=iv  with='v_x_0'' 
629717     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [46] goal: 451, source line: 101, command: 'rule impLeft' 
629718     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [47] goal: 452, source line: 102, command: 'tryclose branch' 
629826     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [48] goal: 453, source line: 103, command: 'instantiate var=iv  with='v_y_0'' 
629828     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [49] goal: 562, source line: 105, command: 'rule impLeft' 
629829     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [50] goal: 563, source line: 106, command: 'tryclose branch' 
629929     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [51] goal: 564, source line: 107, command: 'cut 'v_x_0 = v_y_0'' 
629930     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)'' 
629932     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [53] goal: 676, source line: 111, command: 'rule andRight' 
629934     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [54] goal: 677, source line: 113, command: 'rule andRight' 
629935     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [55] goal: 679, source line: 114, command: 'rule andRight' 
629936     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [56] goal: 681, source line: 115, command: 'rule andRight' 
629939     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [57] goal: 683, source line: 116, command: 'rule lenOfSwap' 
629940     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [58] goal: 685, source line: 117, command: 'tryclose branch' 
629943     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [59] goal: 684, source line: 118, command: 'rule seqNPermSwapNPerm' 
629944     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' 
629946     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [61] goal: 688, source line: 121, command: 'instantiate hide var='jv' with='jv_0'' 
629947     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [62] goal: 689, source line: 122, command: 'rule impLeft' 
629948     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [63] goal: 690, source line: 123, command: 'tryclose branch' 
630039     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [64] goal: 691, source line: 124, command: 'tryclose branch' 
630042     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [65] goal: 682, source line: 125, command: 'rule allRight' 
630043     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [66] goal: 796, source line: 127, command: 'rule impRight' 
630044     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [67] goal: 797, source line: 128, command: 'rule andLeft' 
630045     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [68] goal: 798, source line: 129, command: 'instantiate var=iv with='v_iv_0'' 
630046     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [69] goal: 799, source line: 130, command: 'rule impLeft' 
630050     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [70] goal: 800, source line: 131, command: 'tryclose branch' 
630155     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [71] goal: 801, source line: 132, command: 'rule getOfSwap' 
630156     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [72] goal: 912, source line: 133, command: 'rule ifthenelse_negated' 
630157     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [73] goal: 913, source line: 134, command: 'rule ifthenelse_split occ=0' 
630158     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [74] goal: 914, source line: 135, command: 'rule andLeft' 
630159     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [75] goal: 916, source line: 136, command: 'rule andLeft' 
630160     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [76] goal: 917, source line: 137, command: 'rule andLeft' 
630161     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [77] goal: 918, source line: 138, command: 'rule ifthenelse_split occ=0' 
630162     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [78] goal: 919, source line: 139, command: 'tryclose branch' 
630247     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [79] goal: 920, source line: 140, command: 'rule ifthenelse_split occ=0' 
630248     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [80] goal: 1011, source line: 141, command: 'tryclose branch' 
630330     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [81] goal: 1012, source line: 142, command: 'tryclose branch' 
630334     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [82] goal: 915, source line: 143, command: 'tryclose branch' 
630339     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [83] goal: 680, source line: 144, command: 'rule getOfSwap' 
630340     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [84] goal: 1099, source line: 146, command: 'rule ifthenelse_negated' 
630343     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [85] goal: 1100, source line: 147, command: 'rule ifthenelse_split occ=0' 
630344     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [86] goal: 1101, source line: 148, command: 'rule andLeft' 
630345     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [87] goal: 1103, source line: 149, command: 'rule andLeft' 
630345     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [88] goal: 1104, source line: 150, command: 'rule andLeft' 
630346     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [89] goal: 1105, source line: 151, command: 'rule ifthenelse_split occ=0' 
630347     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [90] goal: 1106, source line: 152, command: 'tryclose branch' 
630354     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [91] goal: 1107, source line: 153, command: 'tryclose branch' 
630358     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [92] goal: 1102, source line: 154, command: 'tryclose branch' 
630447     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [93] goal: 678, source line: 155, command: 'rule getOfSwap' 
630449     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [94] goal: 1225, source line: 157, command: 'rule ifthenelse_negated' 
630451     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [95] goal: 1226, source line: 158, command: 'rule ifthenelse_split occ=0' 
630452     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [96] goal: 1227, source line: 159, command: 'rule andLeft' 
630453     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [97] goal: 1229, source line: 160, command: 'rule andLeft' 
630455     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [98] goal: 1230, source line: 161, command: 'rule andLeft' 
630456     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [99] goal: 1231, source line: 162, command: 'rule ifthenelse_split occ=0' 
630456     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [100] goal: 1232, source line: 163, command: 'tryclose branch' 
630501     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [101] goal: 1233, source line: 164, command: 'tryclose branch' 
630508     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [102] goal: 1228, source line: 165, command: 'tryclose branch' 
630592     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]'' 
630593     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [104] goal: 1397, source line: 169, command: 'rule seqNPermInjective' 
630594     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'' 
630595     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'' 
630596     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [107] goal: 1401, source line: 172, command: 'rule impLeft' 
630597     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [108] goal: 1402, source line: 173, command: 'tryclose branch' 
630719     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [109] goal: 1403, source line: 174, command: 'tryclose branch' 
630723     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'' 
630725     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)'' 
630727     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [112] goal: 1536, source line: 179, command: 'rule andRight' 
630728     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [113] goal: 1537, source line: 181, command: 'rule andRight' 
630730     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [114] goal: 1539, source line: 182, command: 'rule andRight' 
630730     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [115] goal: 1541, source line: 183, command: 'rule andRight' 
630731     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [116] goal: 1543, source line: 184, command: 'tryclose branch' 
630740     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [117] goal: 1544, source line: 185, command: 'rule seqNPermSwapNPerm' 
630745     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'' 
630746     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [119] goal: 1559, source line: 188, command: 'instantiate hide var=jv with='jv_1'' 
630747     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [120] goal: 1560, source line: 189, command: 'tryclose branch' 
630834     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [121] goal: 1542, source line: 190, command: 'rule allRight' 
630836     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [122] goal: 1667, source line: 192, command: 'rule impRight' 
630837     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [123] goal: 1668, source line: 193, command: 'rule andLeft' 
630838     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [124] goal: 1669, source line: 194, command: 'instantiate var=iv with='v_iv_0'' 
630838     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [125] goal: 1670, source line: 195, command: 'rule impLeft' 
630839     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [126] goal: 1671, source line: 196, command: 'tryclose branch' 
630956     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [127] goal: 1672, source line: 197, command: 'rule getOfSwap' 
630957     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [128] goal: 1786, source line: 198, command: 'rule ifthenelse_negated' 
630958     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [129] goal: 1787, source line: 199, command: 'rule ifthenelse_split occ=0' 
630959     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [130] goal: 1788, source line: 200, command: 'rule andLeft' 
630960     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [131] goal: 1790, source line: 201, command: 'rule andLeft' 
630960     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [132] goal: 1791, source line: 202, command: 'rule andLeft' 
630960     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [133] goal: 1792, source line: 203, command: 'rule ifthenelse_split occ=0' 
630961     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [134] goal: 1793, source line: 204, command: 'tryclose branch' 
631048     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [135] goal: 1794, source line: 205, command: 'rule ifthenelse_split occ=0' 
631049     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [136] goal: 1885, source line: 206, command: 'tryclose branch' 
631130     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [137] goal: 1886, source line: 207, command: 'instantiate var=iv with='v_y_0'' 
631130     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [138] goal: 1968, source line: 208, command: 'rule impLeft' 
631131     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [139] goal: 1969, source line: 209, command: 'tryclose branch' 
631135     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [140] goal: 1970, source line: 210, command: 'tryclose branch' 
631139     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [141] goal: 1789, source line: 211, command: 'tryclose branch' 
631144     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [142] goal: 1540, source line: 212, command: 'tryclose branch' 
631273     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [143] goal: 1538, source line: 213, command: 'rule getOfSwap' 
631274     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [144] goal: 2097, source line: 215, command: 'rule ifthenelse_negated' 
631275     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [145] goal: 2098, source line: 216, command: 'rule ifthenelse_split occ=0' 
631276     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [146] goal: 2099, source line: 217, command: 'tryclose branch' 
631286     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [147] goal: 2100, source line: 218, command: 'tryclose branch' 
631382     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [148] goal: 1535, source line: 219, command: 'tryclose branch' 
634747     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'' 
634748     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)'' 
634751     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [151] goal: 4268, source line: 226, command: 'rule andRight' 
634753     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [152] goal: 4269, source line: 228, command: 'rule andRight' 
634753     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [153] goal: 4271, source line: 229, command: 'rule andRight' 
634755     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [154] goal: 4273, source line: 230, command: 'rule andRight' 
634755     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [155] goal: 4275, source line: 231, command: 'tryclose branch' 
634763     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [156] goal: 4276, source line: 232, command: 'rule seqNPermSwapNPerm' 
634764     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'' 
634765     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [158] goal: 4288, source line: 235, command: 'instantiate hide var=jv with='jv_0'' 
634766     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [159] goal: 4289, source line: 236, command: 'rule impLeft' 
634767     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [160] goal: 4290, source line: 237, command: 'tryclose branch' 
634852     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [161] goal: 4291, source line: 238, command: 'tryclose branch' 
634856     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [162] goal: 4274, source line: 239, command: 'rule allRight' 
634857     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [163] goal: 4400, source line: 241, command: 'rule impRight' 
634858     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [164] goal: 4401, source line: 242, command: 'rule andLeft' 
634859     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [165] goal: 4402, source line: 243, command: 'instantiate var=iv with='v_iv_0'' 
634860     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [166] goal: 4403, source line: 244, command: 'rule impLeft' 
634861     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [167] goal: 4404, source line: 245, command: 'tryclose branch' 
634948     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [168] goal: 4405, source line: 246, command: 'rule getOfSwap' 
634950     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [169] goal: 4521, source line: 247, command: 'rule ifthenelse_negated' 
634951     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [170] goal: 4522, source line: 248, command: 'rule ifthenelse_split occ=0' 
634953     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [171] goal: 4523, source line: 249, command: 'rule andLeft' 
634957     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [172] goal: 4525, source line: 250, command: 'rule andLeft' 
634957     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [173] goal: 4526, source line: 251, command: 'rule andLeft' 
634958     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [174] goal: 4527, source line: 252, command: 'rule ifthenelse_split occ=0' 
634959     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [175] goal: 4528, source line: 253, command: 'tryclose branch' 
635034     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [176] goal: 4529, source line: 254, command: 'rule ifthenelse_split occ=0' 
635035     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [177] goal: 4622, source line: 255, command: 'tryclose branch' 
635106     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [178] goal: 4623, source line: 256, command: 'tryclose branch' 
635110     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [179] goal: 4524, source line: 257, command: 'tryclose branch' 
635114     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [180] goal: 4272, source line: 258, command: 'rule getOfSwap' 
635115     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [181] goal: 4713, source line: 260, command: 'rule ifthenelse_negated' 
635116     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [182] goal: 4714, source line: 261, command: 'rule ifthenelse_split occ=0' 
635117     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [183] goal: 4715, source line: 262, command: 'tryclose branch' 
635127     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [184] goal: 4716, source line: 263, command: 'tryclose branch' 
635203     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [185] goal: 4270, source line: 264, command: 'rule getOfSwap' 
635204     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [186] goal: 4839, source line: 266, command: 'rule ifthenelse_negated' 
635205     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [187] goal: 4840, source line: 267, command: 'rule ifthenelse_split occ=0' 
635206     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [188] goal: 4841, source line: 268, command: 'tryclose branch' 
635273     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [189] goal: 4842, source line: 269, command: 'tryclose branch' 
635283     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'' 
635283     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)'' 
635284     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [192] goal: 4950, source line: 275, command: 'rule andRight' 
635286     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [193] goal: 4951, source line: 277, command: 'rule andRight' 
635287     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [194] goal: 4953, source line: 278, command: 'rule andRight' 
635287     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [195] goal: 4955, source line: 279, command: 'rule andRight' 
635288     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [196] goal: 4957, source line: 280, command: 'tryclose branch' 
635299     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [197] goal: 4958, source line: 281, command: 'rule seqNPermSwapNPerm' 
635299     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [198] goal: 4977, source line: 283, command: 'instantiate hide var=iv with='jv_0'' 
635300     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'' 
635301     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [200] goal: 4979, source line: 285, command: 'rule impLeft' 
635302     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [201] goal: 4980, source line: 286, command: 'tryclose branch' 
635432     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))'' 
635433     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [203] goal: 5093, source line: 288, command: 'instantiate hide var=iv with='jv_0'' 
635434     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'' 
635435     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [205] goal: 5095, source line: 290, command: 'rule impLeft' 
635435     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [206] goal: 5096, source line: 291, command: 'tryclose branch' 
635518     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [207] goal: 5097, source line: 292, command: 'tryclose branch' 
635522     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [208] goal: 4956, source line: 293, command: 'rule allRight' 
635523     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [209] goal: 5212, source line: 295, command: 'rule impRight' 
635524     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [210] goal: 5213, source line: 296, command: 'rule andLeft' 
635525     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [211] goal: 5214, source line: 297, command: 'instantiate var=iv with='v_iv_0'' 
635525     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [212] goal: 5215, source line: 300, command: 'rule impLeft' 
635526     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [213] goal: 5216, source line: 301, command: 'tryclose branch' 
635617     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [214] goal: 5217, source line: 302, command: 'rule getOfSwap' 
635618     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [215] goal: 5337, source line: 304, command: 'rule ifthenelse_negated' 
635619     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [216] goal: 5338, source line: 305, command: 'rule ifthenelse_split occ=0' 
635620     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [217] goal: 5339, source line: 306, command: 'rule andLeft' 
635620     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [218] goal: 5341, source line: 307, command: 'rule andLeft' 
635621     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [219] goal: 5342, source line: 308, command: 'rule andLeft' 
635621     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [220] goal: 5343, source line: 309, command: 'rule ifthenelse_split occ=0' 
635622     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [221] goal: 5344, source line: 310, command: 'rule getOfSwap' 
635623     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [222] goal: 5346, source line: 311, command: 'rule ifthenelse_negated' 
635623     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [223] goal: 5347, source line: 312, command: 'rule ifthenelse_split occ=0' 
635624     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [224] goal: 5348, source line: 313, command: 'rule andLeft' 
635625     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [225] goal: 5350, source line: 314, command: 'rule andLeft' 
635625     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [226] goal: 5351, source line: 315, command: 'rule andLeft' 
635626     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [227] goal: 5352, source line: 316, command: 'rule ifthenelse_split occ=0' 
635626     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [228] goal: 5353, source line: 317, command: 'tryclose branch' 
635706     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [229] goal: 5354, source line: 318, command: 'rule ifthenelse_split occ=0' 
635707     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [230] goal: 5463, source line: 319, command: 'tryclose branch' 
635713     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [231] goal: 5464, source line: 320, command: 'tryclose branch' 
635784     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [232] goal: 5349, source line: 321, command: 'tryclose branch' 
635858     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [233] goal: 5345, source line: 322, command: 'rule ifthenelse_split' 
635859     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [234] goal: 5660, source line: 324, command: 'rule getOfSwap' 
635860     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [235] goal: 5662, source line: 325, command: 'rule ifthenelse_negated' 
635861     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [236] goal: 5663, source line: 326, command: 'rule ifthenelse_split occ=0' 
635861     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [237] goal: 5664, source line: 327, command: 'rule andLeft' 
635862     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [238] goal: 5666, source line: 328, command: 'rule andLeft' 
635862     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [239] goal: 5667, source line: 329, command: 'rule andLeft' 
635863     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [240] goal: 5668, source line: 330, command: 'rule ifthenelse_split occ=0' 
635863     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [241] goal: 5669, source line: 331, command: 'tryclose branch' 
635941     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [242] goal: 5670, source line: 332, command: 'tryclose branch' 
635948     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [243] goal: 5665, source line: 333, command: 'tryclose branch' 
636030     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [244] goal: 5661, source line: 334, command: 'rule getOfSwap' 
636031     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [245] goal: 5887, source line: 336, command: 'rule ifthenelse_negated' 
636032     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [246] goal: 5888, source line: 337, command: 'rule ifthenelse_split occ=0' 
636033     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [247] goal: 5889, source line: 338, command: 'rule andLeft' 
636033     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [248] goal: 5891, source line: 339, command: 'rule andLeft' 
636034     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [249] goal: 5892, source line: 340, command: 'rule andLeft' 
636034     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [250] goal: 5893, source line: 341, command: 'rule ifthenelse_split occ=0' 
636034     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [251] goal: 5894, source line: 342, command: 'tryclose branch' 
636039     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [252] goal: 5895, source line: 343, command: 'rule ifthenelse_split occ=0' 
636040     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [253] goal: 5897, source line: 344, command: 'tryclose branch' 
636113     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [254] goal: 5898, source line: 345, command: 'tryclose branch' 
636118     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [255] goal: 5890, source line: 346, command: 'tryclose branch' 
636123     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [256] goal: 5340, source line: 347, command: 'tryclose branch' 
636215     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [257] goal: 4954, source line: 348, command: 'rule getOfSwap' 
636216     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [258] goal: 6115, source line: 350, command: 'rule ifthenelse_negated' 
636216     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [259] goal: 6116, source line: 351, command: 'rule ifthenelse_split occ=0' 
636217     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [260] goal: 6117, source line: 352, command: 'rule andLeft' 
636218     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [261] goal: 6119, source line: 353, command: 'rule andLeft' 
636218     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [262] goal: 6120, source line: 354, command: 'rule andLeft' 
636219     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [263] goal: 6121, source line: 355, command: 'rule ifthenelse_split occ=0' 
636219     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [264] goal: 6122, source line: 356, command: 'tryclose branch' 
636270     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [265] goal: 6123, source line: 357, command: 'rule ifthenelse_split occ=0' 
636271     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [266] goal: 6193, source line: 358, command: 'rule getOfSwap' 
636272     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [267] goal: 6195, source line: 359, command: 'rule ifthenelse_negated' 
636272     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [268] goal: 6196, source line: 360, command: 'rule ifthenelse_split occ=0' 
636273     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [269] goal: 6197, source line: 361, command: 'tryclose branch' 
636278     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [270] goal: 6198, source line: 362, command: 'tryclose branch' 
636283     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [271] goal: 6194, source line: 363, command: 'tryclose branch' 
636394     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [272] goal: 6118, source line: 364, command: 'tryclose branch' 
636476     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [273] goal: 4952, source line: 365, command: 'rule getOfSwap' 
636477     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [274] goal: 6456, source line: 367, command: 'rule ifthenelse_negated' 
636478     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [275] goal: 6457, source line: 368, command: 'rule ifthenelse_split occ=0' 
636478     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [276] goal: 6458, source line: 369, command: 'tryclose branch' 
636635     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [277] goal: 6459, source line: 370, command: 'tryclose branch' 
636718     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'' 
636719     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [279] goal: 6735, source line: 375, command: 'tryclose branch' 
639499     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [280] goal: 6735, source line: 378, command: 'rule seqNPermSwapNPerm' 
639503     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [281] goal: 8783, source line: 380, command: 'instantiate hide var=iv with='jv_1'' 
639504     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'' 
639505     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [283] goal: 8785, source line: 382, command: 'rule impLeft' 
639505     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [284] goal: 8786, source line: 383, command: 'tryclose branch' 
639611     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))'' 
639612     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [286] goal: 8909, source line: 385, command: 'instantiate hide var=iv with='jv_1'' 
639613     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'' 
639613     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [288] goal: 8911, source line: 387, command: 'rule impLeft' 
639614     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [289] goal: 8912, source line: 388, command: 'tryclose branch' 
639712     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [290] goal: 8913, source line: 389, command: 'tryclose branch' 
642419     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [291] goal: 6736, source line: 390, command: 'tryclose branch' 
645325     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [292] goal: 6736, source line: 397, command: 'rule seqNPermSwapNPerm formula='seqNPerm(s_0)'' 
645329     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'' 
645329     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [294] goal: 12634, source line: 400, command: 'instantiate hide var=jv with='jv_0'' 
645330     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [295] goal: 12635, source line: 401, command: 'rule impLeft' 
645331     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [296] goal: 12636, source line: 402, command: 'tryclose branch' 
645436     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))'' 
645437     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'' 
645437     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [299] goal: 12758, source line: 405, command: 'instantiate hide var=jv with='jv_1'' 
645439     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)' ...' 
645439     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [301] goal: 12760, source line: 407, command: 'tryclose branch' 
646492     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm2/Taclet_schiffl_thm_1.proof 
646492     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 106.4ns 
646493     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
648934     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.44s 
648935     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: schiffl_thm_1 
649741     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: schiffl_thm_1 
649742     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 7.8ns 
649743     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [1] goal: 0, source line: 50, command: 'macro split-prop' 
649751     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)'' 
649760     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [3] goal: 11, source line: 52, command: 'instantiate hide var=x with='f_x'' 
649762     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [4] goal: 12, source line: 53, command: 'instantiate hide var=y with='f_y'' 
649764     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [5] goal: 13, source line: 54, command: 'rule impLeft' 
649766     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [6] goal: 14, source line: 55, command: 'tryclose branch' 
649770     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [7] goal: 15, source line: 56, command: 'rule exLeft' 
649771     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [8] goal: 23, source line: 57, command: 'macro split-prop' 
649775     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [9] goal: 27, source line: 58, command: 'rule seqPermDef occ=1' 
649775     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [10] goal: 28, source line: 59, command: 'rule andRight' 
649777     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [11] goal: 29, source line: 60, command: 'tryclose branch' 
649787     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [12] goal: 30, source line: 61, command: 'instantiate hide var=s with='r_0'' 
649787     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [13] goal: 46, source line: 62, command: 'rule andRight' 
649788     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [14] goal: 47, source line: 63, command: 'tryclose branch' 
649834     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [15] goal: 48, source line: 64, command: 'rule allRight' 
649835     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [16] goal: 119, source line: 65, command: 'rule impRight' 
649836     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [17] goal: 120, source line: 66, command: 'instantiate hide var=iv with='iv_0'' 
649836     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [18] goal: 121, source line: 67, command: 'rule impLeft' 
649837     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [19] goal: 122, source line: 68, command: 'tryclose branch' 
649908     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [20] goal: 123, source line: 69, command: 'rule andLeft' 
649908     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [21] goal: 203, source line: 70, command: 'rule seqNPermRange' 
649909     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [22] goal: 204, source line: 71, command: 'instantiate hide var=iv with='iv_0'' 
649910     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [23] goal: 205, source line: 72, command: 'rule impLeft' 
649910     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [24] goal: 206, source line: 73, command: 'tryclose branch' 
649914     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [25] goal: 207, source line: 74, command: 'rule andLeft' 
649915     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [26] goal: 215, source line: 75, command: 'rule andLeft' 
649915     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [27] goal: 216, source line: 76, command: 'rule seqNPermRange' 
649915     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [28] goal: 217, source line: 77, command: 'instantiate hide var=iv with='f_x'' 
649916     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [29] goal: 218, source line: 78, command: 'rule impLeft' 
649917     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [30] goal: 219, source line: 79, command: 'tryclose branch' 
650005     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [31] goal: 220, source line: 80, command: 'rule andLeft' 
650005     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [32] goal: 311, source line: 81, command: 'rule andLeft' 
650006     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [33] goal: 312, source line: 82, command: 'rule seqNPermRange' 
650006     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [34] goal: 313, source line: 83, command: 'instantiate hide var=iv with='f_y'' 
650007     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [35] goal: 314, source line: 84, command: 'rule impLeft' 
650008     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [36] goal: 315, source line: 85, command: 'tryclose branch' 
650096     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [37] goal: 316, source line: 86, command: 'rule andLeft' 
650097     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [38] goal: 410, source line: 87, command: 'rule andLeft' 
650097     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [39] goal: 411, source line: 88, command: 'rule getOfSeqDef occ=0' 
650098     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [40] goal: 412, source line: 89, command: 'rule getOfSeqDef' 
650098     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [41] goal: 413, source line: 90, command: 'rule ifthenelse_split occ=0' 
650099     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [42] goal: 414, source line: 91, command: 'rule andLeft occ=0' 
650099     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [43] goal: 416, source line: 92, command: 'rule sub_zero_2 occ=0' 
650100     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [44] goal: 417, source line: 93, command: 'rule ifthenelse_split occ=2' 
650100     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [45] goal: 418, source line: 94, command: 'rule andLeft' 
650101     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [46] goal: 420, source line: 95, command: 'rule sub_zero_2 occ=0' 
650101     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [47] goal: 421, source line: 96, command: 'rule add_zero_right occ=0' 
650101     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [48] goal: 422, source line: 97, command: 'rule add_zero_right occ=0' 
650102     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [49] goal: 423, source line: 98, command: 'rule add_zero_right occ=0' 
650102     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [50] goal: 424, source line: 99, command: 'rule add_zero_right occ=0' 
650102     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [51] goal: 425, source line: 100, command: 'rule add_zero_right occ=0' 
650103     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [52] goal: 426, source line: 101, command: 'rule add_zero_right occ=0' 
650103     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [53] goal: 427, source line: 102, command: 'rule ifthenelse_split occ=0' 
650103     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [54] goal: 428, source line: 103, command: 'rule ifthenelse_split occ=0' 
650104     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [55] goal: 430, source line: 104, command: 'tryclose branch' 
650106     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [56] goal: 431, source line: 105, command: 'tryclose branch' 
650146     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [57] goal: 429, source line: 106, command: 'rule ifthenelse_split occ=0' 
650147     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [58] goal: 473, source line: 107, command: 'tryclose branch' 
650208     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [59] goal: 474, source line: 108, command: 'rule ifthenelse_split occ=0' 
650209     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [60] goal: 541, source line: 109, command: 'rule seqNPermInjective' 
650209     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [61] goal: 543, source line: 110, command: 'instantiate hide var=iv with='iv_0'' 
650210     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [62] goal: 544, source line: 111, command: 'instantiate hide var=jv with='f_y'' 
650211     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [63] goal: 545, source line: 112, command: 'rule impLeft' 
650212     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [64] goal: 546, source line: 113, command: 'tryclose branch' 
650267     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [65] goal: 547, source line: 114, command: 'tryclose branch' 
650269     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [66] goal: 542, source line: 115, command: 'rule ifthenelse_split occ=0' 
650270     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [67] goal: 606, source line: 116, command: 'rule seqNPermInjective' 
650271     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [68] goal: 608, source line: 117, command: 'instantiate hide var=iv with='iv_0'' 
650272     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [69] goal: 609, source line: 118, command: 'instantiate hide var=jv with='f_x'' 
650273     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [70] goal: 610, source line: 119, command: 'rule impLeft' 
650273     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [71] goal: 611, source line: 120, command: 'tryclose branch' 
650326     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [72] goal: 612, source line: 121, command: 'tryclose branch' 
650328     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [73] goal: 607, source line: 122, command: 'tryclose branch' 
650331     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [74] goal: 419, source line: 123, command: 'tryclose branch' 
650391     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [75] goal: 415, source line: 124, command: 'tryclose branch' 
650442     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_eqSameSeq.proof 
650442     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 96.1ns 
650443     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
652986     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.54s 
652987     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: eqSameSeq 
653864     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: eqSameSeq 
653880     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 12.49ms