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

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

tests
0

failures
0

ignored
10m45.88s

duration
100%

successful

Tests

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

Standard output

290        INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src/test/resources/testcase/dummyTrue.key 
311        DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 8.7ms 
515        INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
527        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)

1420       DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for Meta 
1422       DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for Meta 
1426       DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for Meta 
1426       DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for Meta 
2710       DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for JavaBigintExpression 
7723       DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 7.21s 
7781       INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof dummyTrue.key 
7814       DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 32.7ns 
7827       INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/firstOrder/Taclet_eqTermCut.proof 
7827       DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 179.3ns 
7831       INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
10554      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.72s 
10557      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: eqTermCut 
11583      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: eqTermCut 
11612      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 19.87ms 
11625      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/firstOrder/Taclet_equivAllRight.proof 
11625      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 179ns 
11628      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
14243      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.61s 
14243      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: equivAllRight 
15077      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: equivAllRight 
15089      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 8.59ms 
15092      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_irrflConcrete1.proof 
15093      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 397.9ns 
15094      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
17765      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.67s 
17766      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: irrflConcrete1 
18602      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: irrflConcrete1 
18608      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.52ms 
18611      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_irrflConcrete2.proof 
18612      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 384.4ns 
18613      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
21135      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.52s 
21135      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: irrflConcrete2 
21964      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: irrflConcrete2 
21969      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.17ms 
21974      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_cancel_gtPos.proof 
21974      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 478.5ns 
21976      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
24450      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.47s 
24451      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: cancel_gtPos 
25257      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: cancel_gtPos 
25295      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 34.51ms 
25298      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_cancel_gtNeg.proof 
25300      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 2.03ms 
25302      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
27710      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.41s 
27710      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: cancel_gtNeg 
28504      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: cancel_gtNeg 
28541      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 33.28ms 
28546      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intRulesIgnoringOF/Taclet_moduloIntIsInInt.proof 
28546      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 165ns 
28547      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
30965      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.42s 
30965      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: moduloIntIsInInt 
31767      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: moduloIntIsInInt 
31774      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.25ms 
31778      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intRulesIgnoringOF/Taclet_moduloLongIsInLong.proof 
31778      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 402ns 
31780      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
34218      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.44s 
34218      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: moduloLongIsInLong 
35010      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: moduloLongIsInLong 
35013      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 791.41ns 
35014      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intRulesIgnoringOF/Taclet_moduloShortIsInShort.proof 
35014      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 124.6ns 
35016      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
37423      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.41s 
37423      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: moduloShortIsInShort 
38209      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: moduloShortIsInShort 
38211      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 632.51ns 
38213      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intRulesIgnoringOF/Taclet_moduloByteIsInByte.proof 
38213      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 96.5ns 
38214      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
40586      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.37s 
40586      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: moduloByteIsInByte 
41369      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: moduloByteIsInByte 
41371      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 600.01ns 
41374      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intRulesIgnoringOF/Taclet_moduloCharIsInChar.proof 
41374      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 331.3ns 
41375      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
43753      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.38s 
43754      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: moduloCharIsInChar 
44545      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: moduloCharIsInChar 
44548      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 640.31ns 
44549      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_div_unique1.proof 
44550      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 178.8ns 
44551      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
46968      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.42s 
46968      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: div_unique1 
47746      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: div_unique1 
47782      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 32.25ms 
47784      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_div_unique2.proof 
47784      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 115.8ns 
47785      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
50173      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.39s 
50173      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: div_unique2 
50956      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: div_unique2 
50987      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 26.8ms 
50992      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_div_exists.proof 
50992      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 409.3ns 
50994      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
53415      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.42s 
53416      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: div_exists 
54178      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: div_exists 
54366      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 178.74ms 
54369      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_div_one.proof 
54370      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 136.7ns 
54371      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
56796      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.42s 
56796      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: div_one 
57554      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: div_one 
57558      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.47ms 
57560      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdiv_one.proof 
57560      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 91.8ns 
57561      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
59952      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.39s 
59952      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdiv_one 
60763      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdiv_one 
60774      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 9.36ms 
60777      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_div_zero.proof 
60777      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 531.21ns 
60778      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
63156      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.38s 
63156      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: div_zero 
63937      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: div_zero 
63984      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 43.46ms 
63986      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divResZero1.proof 
63986      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 130.2ns 
63987      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
66403      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.42s 
66403      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divResZero1 
67198      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divResZero1 
67210      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 9.28ms 
67212      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divResZero2.proof 
67212      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 110.9ns 
67213      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
69579      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.37s 
69579      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divResZero2 
70357      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divResZero2 
70368      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 8.6ms 
70370      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divResOne1.proof 
70370      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 123.1ns 
70371      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
72729      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.36s 
72729      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divResOne1 
73505      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divResOne1 
73517      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 9.34ms 
73518      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divResOne2.proof 
73519      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 109.2ns 
73519      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
75872      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.35s 
75872      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divResOne2 
76651      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divResOne2 
76663      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 9.35ms 
76665      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_div_cancel1.proof 
76665      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 96.7ns 
76666      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
79021      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.36s 
79022      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: div_cancel1 
79799      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: div_cancel1 
79817      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 14.7ms 
79821      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_div_cancel2.proof 
79821      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 372.4ns 
79822      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
82180      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.36s 
82180      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: div_cancel2 
82961      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: div_cancel2 
82964      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.19ms 
82967      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divAddMultDenom.proof 
82967      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 301.4ns 
82968      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
85344      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.38s 
85345      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divAddMultDenom 
86125      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divAddMultDenom 
86163      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 30.32ms 
86165      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divMinus.proof 
86169      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 4.48ms 
86171      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
88516      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.35s 
88517      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divMinus 
89289      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divMinus 
89333      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 37.73ms 
89335      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divMinusDenom.proof 
89335      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 104.6ns 
89336      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
91713      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.38s 
91714      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divMinusDenom 
92483      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divMinusDenom 
92513      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 24.38ms 
92514      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divLeastDPos.proof 
92514      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 125.2ns 
92515      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
94914      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.4s 
94915      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divLeastDPos 
95667      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divLeastDPos 
95674      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.64ms 
95676      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divLeastDNeg.proof 
95676      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 107.5ns 
95677      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
98076      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.4s 
98077      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divLeastDNeg 
98829      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divLeastDNeg 
98841      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 8.8ms 
98842      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divGreatestDPos.proof 
98842      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 119.9ns 
98843      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
101224     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.38s 
101224     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divGreatestDPos 
101979     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divGreatestDPos 
101990     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 8.65ms 
101997     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divGreatestDNeg.proof 
101997     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 337.8ns 
101998     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
104389     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.39s 
104389     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divGreatestDNeg 
105166     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divGreatestDNeg 
105174     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.76ms 
105176     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divIncreasingPos.proof 
105176     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 303ns 
105177     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
107541     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.36s 
107541     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divIncreasingPos 
108324     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divIncreasingPos 
108331     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.25ms 
108334     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divIncreasingNeg.proof 
108334     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 296.2ns 
108336     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
110692     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.36s 
110692     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divIncreasingNeg 
111471     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divIncreasingNeg 
111476     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.86ms 
111478     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdiv_zero.proof 
111478     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 81.7ns 
111479     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
113845     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.37s 
113845     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdiv_zero 
114623     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdiv_zero 
114626     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.28ms 
114629     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdivPulloutMinusNum.proof 
114629     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 306.7ns 
114630     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
116987     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.36s 
116987     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdivPulloutMinusNum 
117766     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdivPulloutMinusNum 
117775     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 6.52ms 
117778     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdivPulloutMinusDenom.proof 
117778     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 358.2ns 
117779     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
120133     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.35s 
120133     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdivPulloutMinusDenom 
120910     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdivPulloutMinusDenom 
120947     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 30.5ms 
120949     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdiv_uniquePosPos.proof 
120949     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 112.3ns 
120951     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
123339     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.39s 
123339     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdiv_uniquePosPos 
124113     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdiv_uniquePosPos 
124127     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 11.14ms 
124129     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdiv_uniquePosNeg.proof 
124129     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 240.5ns 
124130     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
126488     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.36s 
126489     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdiv_uniquePosNeg 
127265     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdiv_uniquePosNeg 
127279     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 10.47ms 
127280     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdiv_uniqueNegPos.proof 
127280     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 91.3ns 
127281     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
129625     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.34s 
129625     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdiv_uniqueNegPos 
130399     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdiv_uniqueNegPos 
130412     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 10.69ms 
130414     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdiv_uniqueNegNeg.proof 
130414     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 111.7ns 
130415     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
132794     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.38s 
132794     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdiv_uniqueNegNeg 
133595     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdiv_uniqueNegNeg 
133608     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 9.99ms 
133609     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdivMultDenom1.proof 
133609     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 115.5ns 
133610     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
135983     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.37s 
135983     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdivMultDenom1 
136732     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdivMultDenom1 
136761     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 24.57ms 
136763     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdivMultDenom2.proof 
136763     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 92ns 
136764     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
139226     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.46s 
139227     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdivMultDenom2 
139976     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdivMultDenom2 
139978     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 933.11ns 
139980     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_mod_geZero.proof 
139980     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 74.5ns 
139981     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
142350     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.37s 
142350     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: mod_geZero 
143098     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: mod_geZero 
143101     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.69ms 
143103     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_mod_lessDenom.proof 
143103     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 79.1ns 
143103     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
145477     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.37s 
145477     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: mod_lessDenom 
146227     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: mod_lessDenom 
146233     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.44ms 
146235     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmod_NumPos.proof 
146235     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 92.2ns 
146235     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
148607     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.37s 
148608     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmod_NumPos 
149377     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmod_NumPos 
149384     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.66ms 
149385     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmod_NumNeg.proof 
149385     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 80.3ns 
149386     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
151726     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.34s 
151726     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmod_NumNeg 
152494     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmod_NumNeg 
152509     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 11.97ms 
152510     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmod_geZero.proof 
152510     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 84.1ns 
152511     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
154846     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.34s 
154846     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmod_geZero 
155621     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmod_geZero 
155629     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.75ms 
155630     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmodNumZero.proof 
155630     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 79ns 
155631     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
158010     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.38s 
158010     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmodNumZero 
158791     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmodNumZero 
158793     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.12ms 
158796     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmod_pulloutminusNum.proof 
158796     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 279.7ns 
158797     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
161145     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.35s 
161146     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmod_pulloutminusNum 
161916     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmod_pulloutminusNum 
161920     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.33ms 
161921     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmod_pulloutminusDenom.proof 
161921     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 73.2ns 
161922     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
164258     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.34s 
164259     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmod_pulloutminusDenom 
165028     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmod_pulloutminusDenom 
165031     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.58ms 
165032     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmodUnique1.proof 
165032     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 75.1ns 
165033     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
167367     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.33s 
167368     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmodUnique1 
168140     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmodUnique1 
168193     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 44.27ms 
168194     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmodUnique2.proof 
168194     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 103.7ns 
168195     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
170531     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.34s 
170532     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmodUnique2 
171300     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmodUnique2 
171367     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 57.4ms 
171371     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_intDivRem.proof 
171371     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 341ns 
171372     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
173729     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.36s 
173729     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: intDivRem 
174496     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: intDivRem 
174499     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.27ms 
174501     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmodjmod.proof 
174501     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 90.9ns 
174502     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
176927     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.43s 
176929     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmodjmod 
177735     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmodjmod 
177766     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 27.77ms 
177769     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmodDivisible.proof 
177773     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 4.3ms 
177775     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
180142     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.37s 
180142     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmodDivisible 
180890     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmodDivisible 
180910     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 16.69ms 
180913     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmodDivisibleRep.proof 
180913     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 274.4ns 
180914     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
183351     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.44s 
183351     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmodDivisibleRep 
184119     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmodDivisibleRep 
184122     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 854.91ns 
184123     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdivAddMultDenom.proof 
184123     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 63ns 
184124     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
186490     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.37s 
186490     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdivAddMultDenom 
187234     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdivAddMultDenom 
187360     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 114.63ms 
187363     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmodAltZero.proof 
187363     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 252.2ns 
187364     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
189693     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.33s 
189693     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmodAltZero 
190467     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmodAltZero 
190476     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 6.25ms 
190477     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmodAddMultDenomZero.proof 
190477     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 72.7ns 
190478     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
192827     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.35s 
192827     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmodAddMultDenomZero 
193600     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmodAddMultDenomZero 
193606     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.04ms 
193607     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_polyDiv_zero.proof 
193607     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 61.5ns 
193608     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
195948     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.34s 
195948     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: polyDiv_zero 
196718     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: polyDiv_zero 
196731     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 10.64ms 
196734     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_polyMod_ltdivDenom.proof 
196734     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 258.4ns 
196735     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
199073     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.34s 
199073     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: polyMod_ltdivDenom 
199840     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: polyMod_ltdivDenom 
199850     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.57ms 
199852     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_empty.proof 
199852     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 64.3ns 
199853     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
202185     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.33s 
202185     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_empty 
202952     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_empty 
202956     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.76ms 
202958     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_induction_upper.proof 
202958     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 75.2ns 
202959     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
205297     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.34s 
205297     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_upper 
206065     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_induction_upper 
206069     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.87ms 
206070     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_induction_lower.proof 
206070     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 74.4ns 
206071     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
208400     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.33s 
208400     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_lower 
209181     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_induction_lower 
209195     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 10.98ms 
209196     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_bounds.proof 
209196     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 75ns 
209197     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
211543     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.35s 
211543     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_bounds 
212311     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_bounds 
212323     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 8.53ms 
212324     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_bounds2.proof 
212324     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 65.8ns 
212325     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
214667     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.34s 
214667     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_bounds2 
215433     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_bounds2 
215444     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 8.4ms 
215445     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_induction_upper2.proof 
215445     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 70.1ns 
215446     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
217805     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.36s 
217805     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_upper2 
218551     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_induction_upper2 
218554     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.03ms 
218556     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_induction_upper_concrete.proof 
218556     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 72.5ns 
218556     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
220908     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.35s 
220908     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_upper_concrete 
221653     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_induction_upper_concrete 
221656     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.33ms 
221657     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_induction_upper_concrete_2.proof 
221657     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 66.3ns 
221658     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
224014     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.36s 
224014     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_upper_concrete_2 
224756     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_induction_upper_concrete_2 
224760     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.53ms 
224762     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_induction_upper2_concrete.proof 
224762     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 65.6ns 
224762     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
227166     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.4s 
227167     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_upper2_concrete 
227961     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_induction_upper2_concrete 
227966     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.56ms 
227968     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_induction_lower_concrete.proof 
227968     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 220.9ns 
227969     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
230333     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.36s 
230333     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_lower_concrete 
231105     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_induction_lower_concrete 
231107     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 461.7ns 
231108     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_induction_lower2.proof 
231108     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 65.6ns 
231109     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
233450     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.34s 
233450     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_lower2 
234217     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_induction_lower2 
234220     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.73ms 
234221     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_induction_lower2_concrete.proof 
234221     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 58ns 
234222     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
236571     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.35s 
236572     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_lower2_concrete 
237339     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_induction_lower2_concrete 
237341     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 799.61ns 
237342     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_positive.proof 
237343     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 65.2ns 
237343     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
239683     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.34s 
239686     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_positive 
240472     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_positive 
240503     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 27.87ms 
240506     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_upper_bound.proof 
240506     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 233.3ns 
240507     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
242847     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.34s 
242848     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_upper_bound 
243615     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_upper_bound 
243640     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 22.59ms 
243642     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_lower_bound.proof 
243642     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 122.1ns 
243643     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
245970     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.33s 
245970     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_lower_bound 
246738     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_lower_bound 
246758     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 17.2ms 
246759     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_positive_lower_bound_element.proof 
246759     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 70.4ns 
246760     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
249108     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.35s 
249108     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_positive_lower_bound_element 
249874     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_positive_lower_bound_element 
249901     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 23.3ms 
249903     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_sub_same_index.proof 
249903     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 73.3ns 
249903     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
252233     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.33s 
252233     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_sub_same_index 
253001     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_sub_same_index 
253019     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 15.03ms 
253021     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_less_same_index.proof 
253021     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 79.4ns 
253021     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
255382     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.36s 
255382     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_less_same_index 
256149     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_less_same_index 
256183     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 29.34ms 
256184     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_equal_except_one_index.proof 
256184     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 73ns 
256185     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
258519     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.33s 
258519     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_equal_except_one_index 
259288     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_equal_except_one_index 
259306     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 14.24ms 
259310     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_is_max.proof 
259311     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 227ns 
259312     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
261678     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.37s 
261678     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_is_max 
262425     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_is_max 
262438     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 9.99ms 
262439     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_is_max2.proof 
262439     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 68.7ns 
262440     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
264849     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.41s 
264850     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_is_max2 
265596     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_is_max2 
265615     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 16.27ms 
265617     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_is_max3.proof 
265617     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 77ns 
265617     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
268001     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.38s 
268002     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_is_max3 
268748     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_is_max3 
268761     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 10.09ms 
268762     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_is_max4.proof 
268762     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 74.7ns 
268763     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
271134     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.37s 
271135     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_is_max4 
271885     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_is_max4 
271939     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 50.27ms 
271941     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_lt_max.proof 
271941     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 77.2ns 
271942     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
274310     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.37s 
274310     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_lt_max 
275081     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_lt_max 
275097     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 12.61ms 
275098     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_lt_max2.proof 
275098     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 99.3ns 
275099     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
277442     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.34s 
277442     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_lt_max2 
278212     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_lt_max2 
278228     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 13.09ms 
278230     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_lt_max3.proof 
278230     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 73.8ns 
278231     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
280578     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.35s 
280578     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_lt_max3 
281355     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_lt_max3 
281370     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 11.86ms 
281373     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_lt_max4.proof 
281373     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 236.3ns 
281374     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
283717     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.34s 
283717     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_lt_max4 
284487     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_lt_max4 
284501     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 11.02ms 
284502     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_gt0.proof 
284502     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 71.9ns 
284503     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
286837     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.33s 
286837     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_gt0 
287604     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_gt0 
287620     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 13.13ms 
287621     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_gt0_alt.proof 
287622     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 61.3ns 
287622     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
290011     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.39s 
290011     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_gt0_alt 
290780     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_gt0_alt 
290795     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 12.24ms 
290797     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_add_concrete.proof 
290797     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 74.8ns 
290797     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
293130     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.33s 
293130     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_add_concrete 
293898     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_add_concrete 
293904     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.72ms 
293905     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bprod/Taclet_bprod_all_positive.proof 
293905     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 54.7ns 
293906     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
296230     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.32s 
296230     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bprod_all_positive 
297059     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bprod_all_positive 
297071     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 9.07ms 
297072     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bprod/Taclet_bprod_split.proof 
297072     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 54.3ns 
297073     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
299410     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.34s 
299410     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bprod_split 
300179     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bprod_split 
300183     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.89ms 
300184     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powConcrete0.proof 
300185     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 191.3ns 
300185     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
302571     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.39s 
302571     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powConcrete0 
303318     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powConcrete0 
303320     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 577.51ns 
303322     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powConcrete1.proof 
303322     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 65.7ns 
303322     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
305678     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.36s 
305678     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powConcrete1 
306424     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powConcrete1 
306427     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 838.31ns 
306428     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powSplitFactor.proof 
306428     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 54.8ns 
306429     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
308789     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.36s 
308789     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powSplitFactor 
309535     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powSplitFactor 
309541     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.28ms 
309542     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powAdd.proof 
309542     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 78.7ns 
309543     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
311892     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.35s 
311892     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powAdd 
312638     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powAdd 
312643     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.23ms 
312645     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powMono.proof 
312645     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 53.9ns 
312645     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
314999     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.35s 
314999     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powMono 
315767     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powMono 
315777     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 7.77ms 
315778     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powMonoConcrete.proof 
315778     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 71.2ns 
315779     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
318113     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.33s 
318114     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powMonoConcrete 
318881     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powMonoConcrete 
318885     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.62ms 
318886     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powMonoConcreteRight.proof 
318886     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 52.2ns 
318886     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
321226     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.34s 
321226     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powMonoConcreteRight 
321996     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powMonoConcreteRight 
321998     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 480ns 
322000     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powPositive.proof 
322000     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 186.9ns 
322001     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
324340     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.34s 
324341     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powPositive 
325118     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powPositive 
325124     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.21ms 
325125     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powPositiveConcrete.proof 
325125     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 66.8ns 
325126     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
327469     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.34s 
327470     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powPositiveConcrete 
328239     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powPositiveConcrete 
328241     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 507.64ns 
328242     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powGeq1Concrete.proof 
328242     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 52.8ns 
328242     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
330574     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.33s 
330574     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powGeq1Concrete 
331344     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powGeq1Concrete 
331346     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 469.9ns 
331347     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_pow2InIntLower.proof 
331347     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 63.6ns 
331348     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
333683     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.34s 
333683     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: pow2InIntLower 
334452     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: pow2InIntLower 
334454     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 473.9ns 
334455     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_pow2InIntUpper.proof 
334455     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 65.3ns 
334456     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
336786     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.33s 
336786     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: pow2InIntUpper 
337556     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: pow2InIntUpper 
337559     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.64ms 
337560     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logSelfConcrete.proof 
337561     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 52.5ns 
337561     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
339895     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.33s 
339895     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logSelfConcrete 
340663     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logSelfConcrete 
340670     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.53ms 
340671     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_log1Concrete.proof 
340671     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 50.4ns 
340672     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
342997     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.33s 
342997     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: log1Concrete 
343799     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: log1Concrete 
343802     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.58ms 
343804     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logProduct.proof 
343804     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 62.6ns 
343804     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
346165     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.36s 
346165     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logProduct 
346913     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logProduct 
346919     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.33ms 
346920     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logTimesBaseConcrete.proof 
346920     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 54.8ns 
346921     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
349277     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.36s 
349277     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logTimesBaseConcrete 
350024     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logTimesBaseConcrete 
350028     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2ms 
350029     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logProdIdentity.proof 
350029     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 79.1ns 
350030     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
352384     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.35s 
352384     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logProdIdentity 
353131     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logProdIdentity 
353144     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 9.48ms 
353145     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logProdIdentityConcrete.proof 
353145     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 71ns 
353146     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
355518     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.37s 
355518     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logProdIdentityConcrete 
356265     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logProdIdentityConcrete 
356268     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.48ms 
356269     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logPowIdentity.proof 
356269     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 52.8ns 
356270     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
358623     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.35s 
358624     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logPowIdentity 
359395     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logPowIdentity 
359398     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.03ms 
359399     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logPowIdentityConcrete.proof 
359399     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 54.5ns 
359400     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
361736     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.34s 
361736     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logPowIdentityConcrete 
362507     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logPowIdentityConcrete 
362511     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.82ms 
362512     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logPositive.proof 
362512     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 51.8ns 
362512     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
364871     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.36s 
364871     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logPositive 
365640     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logPositive 
365652     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 9.81ms 
365653     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logPositiveConcrete.proof 
365653     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 69.8ns 
365654     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
367988     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.33s 
367988     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logPositiveConcrete 
368756     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logPositiveConcrete 
368760     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 296.01ns 
368762     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logMono.proof 
368762     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 64.2ns 
368763     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
371095     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.33s 
371095     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logMono 
371873     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logMono 
371899     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 20.97ms 
371900     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logMonoConcrete.proof 
371900     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 58.8ns 
371901     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
374245     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.34s 
374245     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logMonoConcrete 
375030     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logMonoConcrete 
375033     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.37ms 
375035     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powLogLess.proof 
375035     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 56.2ns 
375035     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
377367     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.33s 
377367     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powLogLess 
378137     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powLogLess 
378151     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 11.54ms 
378152     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powLogMore2.proof 
378153     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 68.5ns 
378153     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
380486     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.33s 
380486     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powLogMore2 
381271     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powLogMore2 
381290     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 13.24ms 
381293     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logLessThanPow.proof 
381293     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 227.71ns 
381294     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
383641     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.35s 
383641     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logLessThanPow 
384409     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logLessThanPow 
384426     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 14.14ms 
384427     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logLessThanPowConcrete.proof 
384427     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 70.2ns 
384428     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
386778     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.35s 
386778     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logLessThanPowConcrete 
387551     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logLessThanPowConcrete 
387554     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 535.01ns 
387556     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logSqueeze.proof 
387556     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 187.9ns 
387557     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
389915     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.36s 
389915     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logSqueeze 
390662     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logSqueeze 
390667     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.2ms 
390668     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/booleanRules/Taclet_ifthenelse_equals.proof 
390668     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 70.5ns 
390669     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
393061     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.39s 
393061     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: ifthenelse_equals 
393861     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: ifthenelse_equals 
393864     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.48ms 
393865     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/booleanRules/Taclet_ifthenelse_equals_1.proof 
393865     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 63.7ns 
393866     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
396219     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.35s 
396219     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: ifthenelse_equals_1 
396971     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: ifthenelse_equals_1 
396973     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 714.91ns 
396975     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/booleanRules/Taclet_ifthenelse_equals_2.proof 
396975     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 58.5ns 
396975     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
399341     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.37s 
399342     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: ifthenelse_equals_2 
400095     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: ifthenelse_equals_2 
400098     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 667.11ns 
400099     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/locSet/Taclet_disjointWithSingleton1.proof 
400099     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 53.5ns 
400100     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
402454     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.35s 
402454     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: disjointWithSingleton1 
403230     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: disjointWithSingleton1 
403234     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.3ms 
403235     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/locSet/Taclet_disjointWithSingleton2.proof 
403236     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 59.5ns 
403236     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
405603     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.37s 
405603     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: disjointWithSingleton2 
406381     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: disjointWithSingleton2 
406384     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.11ms 
406385     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/locSet/Taclet_disjointArrayRanges.proof 
406385     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 57.5ns 
406386     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
408719     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.33s 
408720     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: disjointArrayRanges 
409494     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: disjointArrayRanges 
409501     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 5.02ms 
409503     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/locSet/Taclet_disjointArrayRangeAllFields1.proof 
409503     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 62.3ns 
409504     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
411837     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.33s 
411837     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: disjointArrayRangeAllFields1 
412614     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: disjointArrayRangeAllFields1 
412620     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.37ms 
412621     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/locSet/Taclet_disjointArrayRangeAllFields2.proof 
412621     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 58.1ns 
412622     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
414955     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.33s 
414955     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: disjointArrayRangeAllFields2 
415740     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: disjointArrayRangeAllFields2 
415746     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.1ms 
415747     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqSelfDefinition.proof 
415747     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 60.5ns 
415748     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
418129     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.38s 
418129     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqSelfDefinition 
418888     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqSelfDefinition 
418895     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 5.34ms 
418896     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqOutsideValue.proof 
418897     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 64.4ns 
418897     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
421260     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.36s 
421260     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqOutsideValue 
422018     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqOutsideValue 
422022     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.9ms 
422023     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_castedGetAny.proof 
422023     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 60.8ns 
422024     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
424371     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.35s 
424371     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: castedGetAny 
425151     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: castedGetAny 
425155     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.13ms 
425156     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqGetAlphaCast.proof 
425156     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 51.1ns 
425156     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
427485     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.33s 
427485     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqGetAlphaCast 
428269     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqGetAlphaCast 
428272     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 680.81ns 
428273     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqSingleton.proof 
428273     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 63.8ns 
428273     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
430598     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.32s 
430599     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqSingleton 
431380     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqSingleton 
431382     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 953.51ns 
431383     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqSingletonConcrete.proof 
431384     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 73.3ns 
431384     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
433710     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.33s 
433710     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqSingletonConcrete 
434490     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqSingletonConcrete 
434492     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 870.81ns 
434493     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqConcat.proof 
434493     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 77.2ns 
434494     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
436840     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.35s 
436840     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqConcat 
437598     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqConcat 
437606     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 6.15ms 
437608     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqSub.proof 
437608     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 71.9ns 
437608     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
439962     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.35s 
439962     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqSub 
440745     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqSub 
440748     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.16ms 
440749     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqReverse.proof 
440749     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 62.1ns 
440750     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
443081     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.33s 
443081     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqReverse 
443864     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqReverse 
443870     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.88ms 
443872     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqEmpty.proof 
443872     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 191ns 
443873     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
446213     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.34s 
446213     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqEmpty 
446994     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqEmpty 
446996     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 794.01ns 
446997     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqSingleton.proof 
446998     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 60.4ns 
446998     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
449324     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.33s 
449324     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqSingleton 
450105     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqSingleton 
450107     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 622.81ns 
450108     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqConcat.proof 
450108     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 62.7ns 
450109     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
452457     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.35s 
452457     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqConcat 
453215     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqConcat 
453218     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.21ms 
453219     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqSub.proof 
453219     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 65.4ns 
453220     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
455571     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.35s 
455571     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqSub 
456353     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqSub 
456355     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 693.81ns 
456357     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqReverse.proof 
456357     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 62.2ns 
456357     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
458691     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.33s 
458691     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqReverse 
459473     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqReverse 
459475     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 927.01ns 
459477     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_equalityToSeqGetAndSeqLenLeft.proof 
459477     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 61.1ns 
459477     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
462044     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.57s 
462045     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: equalityToSeqGetAndSeqLenLeft 
462843     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: equalityToSeqGetAndSeqLenLeft 
462845     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 912.61ns 
462847     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_equalityToSeqGetAndSeqLenRight.proof 
462847     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 73ns 
462847     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
465199     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.35s 
465199     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: equalityToSeqGetAndSeqLenRight 
465980     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: equalityToSeqGetAndSeqLenRight 
465983     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.93ms 
465984     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqSingletonEQ.proof 
465985     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 60.6ns 
465985     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
468330     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.34s 
468330     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqSingletonEQ 
469112     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqSingletonEQ 
469114     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 828.61ns 
469116     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqConcatEQ.proof 
469116     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 73.7ns 
469116     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
471545     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.43s 
471545     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqConcatEQ 
472333     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqConcatEQ 
472341     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 6.08ms 
472342     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqSubEQ.proof 
472342     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 53.4ns 
472343     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
474705     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.36s 
474706     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqSubEQ 
475468     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqSubEQ 
475470     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 537.41ns 
475471     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqReverseEQ.proof 
475471     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 60.4ns 
475472     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
477821     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.35s 
477822     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqReverseEQ 
478603     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqReverseEQ 
478608     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.59ms 
478609     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqEmptyEQ.proof 
478610     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 60.6ns 
478610     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
480938     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.33s 
480938     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqEmptyEQ 
481720     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqEmptyEQ 
481723     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 829.21ns 
481724     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqSingletonEQ.proof 
481724     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 49.5ns 
481725     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
484075     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.35s 
484076     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqSingletonEQ 
484834     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqSingletonEQ 
484836     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 633.51ns 
484838     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqConcatEQ.proof 
484838     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 67.9ns 
484838     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
487194     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.36s 
487194     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqConcatEQ 
487978     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqConcatEQ 
487981     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.69ms 
487983     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqSubEQ.proof 
487983     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 57.7ns 
487983     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
490314     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.33s 
490314     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqSubEQ 
491199     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqSubEQ 
491202     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 771.41ns 
491203     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqReverseEQ.proof 
491203     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 61.5ns 
491204     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
493547     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.34s 
493547     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqReverseEQ 
494332     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqReverseEQ 
494335     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.15ms 
494336     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqDefEQ.proof 
494336     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 52.2ns 
494337     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
496660     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.32s 
496660     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqDefEQ 
497441     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqDefEQ 
497444     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.09ms 
497448     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqDefEQ.proof 
497448     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 66.7ns 
497449     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
499789     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.34s 
499789     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqDefEQ 
500546     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqDefEQ 
500550     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.98ms 
500551     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqConcatWithSeqEmpty1.proof 
500551     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 62ns 
500552     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
502893     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.34s 
502893     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqConcatWithSeqEmpty1 
503673     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqConcatWithSeqEmpty1 
503680     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 5.08ms 
503681     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqConcatWithSeqEmpty2.proof 
503681     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 63.9ns 
503682     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
506006     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.32s 
506006     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqConcatWithSeqEmpty2 
506784     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqConcatWithSeqEmpty2 
506792     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 5.33ms 
506793     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqReverseOfSeqEmpty.proof 
506793     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 60.1ns 
506794     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
509133     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.34s 
509133     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqReverseOfSeqEmpty 
509911     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqReverseOfSeqEmpty 
509916     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.96ms 
509918     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_subSeqComplete.proof 
509918     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 50.8ns 
509919     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
512255     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.34s 
512257     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: subSeqComplete 
513037     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: subSeqComplete 
513043     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.98ms 
513044     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_subSeqTailR.proof 
513044     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 59.9ns 
513045     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
515388     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.34s 
515388     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: subSeqTailR 
516147     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: subSeqTailR 
516157     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 7.56ms 
516158     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_subSeqTailL.proof 
516159     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 64.7ns 
516159     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
518521     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.36s 
518521     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: subSeqTailL 
519302     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: subSeqTailL 
519311     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 7.33ms 
519313     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_subSeqTailEQR.proof 
519313     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 61ns 
519313     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
521663     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.35s 
521663     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: subSeqTailEQR 
522423     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: subSeqTailEQR 
522432     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 6.67ms 
522433     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_subSeqTailEQL.proof 
522433     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 48.8ns 
522434     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
524782     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.35s 
524782     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: subSeqTailEQL 
525565     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: subSeqTailEQL 
525579     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 11.86ms 
525581     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDef_split.proof 
525581     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 201.5ns 
525582     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
527937     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.36s 
527937     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_split 
528699     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDef_split 
528717     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 15.17ms 
528719     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDef_induction_upper.proof 
528719     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 57.9ns 
528720     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
531073     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.35s 
531073     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_induction_upper 
531856     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDef_induction_upper 
531876     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 16.7ms 
531877     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDef_induction_upper_concrete.proof 
531877     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 72.1ns 
531878     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
534228     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.35s 
534228     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_induction_upper_concrete 
534989     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDef_induction_upper_concrete 
535007     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 15.13ms 
535009     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDef_induction_lower.proof 
535009     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 60ns 
535009     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
537398     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.39s 
537398     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_induction_lower 
538179     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDef_induction_lower 
538197     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 14.1ms 
538198     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDef_induction_lower_concrete.proof 
538198     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 57.9ns 
538199     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
540552     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.35s 
540552     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_induction_lower_concrete 
541312     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDef_induction_lower_concrete 
541330     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 14.63ms 
541331     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDef_split_in_three.proof 
541331     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 66.9ns 
541332     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
543675     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.34s 
543676     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_split_in_three 
544458     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDef_split_in_three 
544504     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 37.91ms 
544505     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDef_empty.proof 
544506     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 55ns 
544506     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
546895     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.39s 
546895     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_empty 
547680     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDef_empty 
547684     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.55ms 
547686     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDef_one_summand.proof 
547686     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 52.5ns 
547686     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
550059     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.37s 
550060     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_one_summand 
550841     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDef_one_summand 
550845     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.84ms 
550847     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDef_lower_equals_upper.proof 
550847     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 59.8ns 
550847     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
553193     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.35s 
553193     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_lower_equals_upper 
553982     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDef_lower_equals_upper 
553985     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.7ms 
553986     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDefOfSeq.proof 
553986     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 49.6ns 
553987     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
556362     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.37s 
556362     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDefOfSeq 
557185     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDefOfSeq 
557197     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 9.23ms 
557198     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqSelfDefinitionEQ2.proof 
557198     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 62ns 
557199     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
559545     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.35s 
559545     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqSelfDefinitionEQ2 
560326     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqSelfDefinitionEQ2 
560332     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.96ms 
560333     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_indexOfSeqSingleton.proof 
560333     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 51.8ns 
560334     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
562682     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.35s 
562682     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: indexOfSeqSingleton 
563441     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: indexOfSeqSingleton 
563444     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.26ms 
563445     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_indexOfSeqConcatFirst.proof 
563445     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 62.5ns 
563446     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
565803     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.36s 
565803     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: indexOfSeqConcatFirst 
566587     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: indexOfSeqConcatFirst 
566597     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 7.47ms 
566598     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_indexOfSeqConcatSecond.proof 
566598     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 71.6ns 
566599     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
568962     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.36s 
568962     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: indexOfSeqConcatSecond 
569749     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: indexOfSeqConcatSecond 
569760     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 8.02ms 
569761     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_indexOfSeqSub.proof 
569761     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 69.6ns 
569761     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
572115     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.35s 
572115     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: indexOfSeqSub 
572878     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: indexOfSeqSub 
572890     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 10.06ms 
572892     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfArray2seq.proof 
572892     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 64.8ns 
572892     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
575258     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.37s 
575258     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfArray2seq 
576038     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfArray2seq 
576040     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 907.91ns 
576041     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getAnyOfArray2seq.proof 
576041     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 49.8ns 
576042     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
578394     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.35s 
578394     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getAnyOfArray2seq 
579178     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getAnyOfArray2seq 
579181     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.53ms 
579182     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfArray2seq.proof 
579182     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 64.7ns 
579183     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
581525     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.34s 
581525     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfArray2seq 
582286     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfArray2seq 
582292     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.77ms 
582293     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_getAnyOfNPermInv.proof 
582293     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 65ns 
582293     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
584639     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.35s 
584639     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getAnyOfNPermInv 
585427     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getAnyOfNPermInv 
585431     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.46ms 
585433     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqNPermRange.proof 
585433     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 203ns 
585434     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
587781     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.35s 
587781     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqNPermRange 
588563     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqNPermRange 
588602     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 33.14ms 
588603     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermTrans.proof 
588603     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 60.7ns 
588604     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
590954     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.35s 
590954     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermTrans 
591746     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermTrans 
591762     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 13.28ms 
591764     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermRefl.proof 
591764     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 63.1ns 
591764     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
594127     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.36s 
594127     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermRefl 
594909     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermRefl 
594919     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 8.34ms 
594920     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermSplit.proof 
594921     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 78.1ns 
594921     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
597329     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.41s 
597329     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermSplit 
598112     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermSplit 
598114     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 149.8ns 
598115     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqNPermRight.proof 
598115     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 49.6ns 
598117     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
600490     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.37s 
600490     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqNPermRight 
601274     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqNPermRight 
601353     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 68.13ms 
601355     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermFromSwap.proof 
601355     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 65ns 
601356     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
603701     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.35s 
603701     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermFromSwap 
604483     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermFromSwap 
604515     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 27.46ms 
604517     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermTransAlt0.proof 
604517     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 55ns 
604517     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
606866     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.35s 
606866     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermTransAlt0 
607630     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermTransAlt0 
607632     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 262.7ns 
607633     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermTransAlt1.proof 
607633     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 50.8ns 
607634     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
609985     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.35s 
609987     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermTransAlt1 
610772     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermTransAlt1 
610773     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 195.4ns 
610775     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermTransAlt2.proof 
610775     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 61.1ns 
610775     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
613125     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.35s 
613125     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermTransAlt2 
613908     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermTransAlt2 
613910     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 193.9ns 
613911     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermTransAlt3.proof 
613911     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 49ns 
613911     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
616248     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.34s 
616248     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermTransAlt3 
617032     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermTransAlt3 
617034     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 314.2ns 
617035     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermForall.proof 
617035     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 65.6ns 
617036     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
619381     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.35s 
619381     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermForall 
620164     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermForall 
620265     INFO  Test worker     d.u.i.k.s.SMTFocusResults Analyzing unsat core: (L_1 L_3 L_4) 
620279     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 113.1ms 
620282     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermExists.proof 
620282     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 219.2ns 
620283     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
622647     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.36s 
622647     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermExists 
623410     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermExists 
623458     INFO  Test worker     d.u.i.k.s.SMTFocusResults Analyzing unsat core: (L_1 L_3 L_5 L_6 L_7) 
623459     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 46.49ms 
623460     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm2/Taclet_schiffl_lemma_2.proof 
623460     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 60.8ns 
623461     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
625808     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.35s 
625809     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: schiffl_lemma_2 
626591     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: schiffl_lemma_2 
626593     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.4ns 
626622     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 1: 'macro split-prop' on goal 0 (script from line 49) 
626653     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 2: 'rule allRight' on goal 3 (script from line 50) 
626666     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 3: 'rule allRight' on goal 4 (script from line 51) 
626670     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 4: 'macro split-prop' on goal 5 (script from line 52) 
626680     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 5: 'rule 'seqPermDefLeft'' on goal 11 (script from line 53) 
626681     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 6: 'rule 'andLeft'' on goal 12 (script from line 54) 
626683     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 7: 'rule 'exLeft'' on goal 13 (script from line 55) 
626684     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 8: 'macro split-prop' on goal 14 (script from line 56) 
626688     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 9: 'rule  seqNPermRange' on goal 16 (script from line 58) 
626689     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 10: 'instantiate var=iv with='v_x_0' occ=1' on goal 17 (script from line 59) 
626691     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 11: 'rule impLeft' on goal 18 (script from line 60) 
626693     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 12: 'tryclose branch' on goal 19 (script from line 61) 
626889     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 13: 'rule andLeft' on goal 20 (script from line 62) 
626890     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 14: 'rule andLeft' on goal 97 (script from line 63) 
626892     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 15: 'instantiate var=iv with='v_y_0' occ=1' on goal 98 (script from line 65) 
626893     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 16: 'rule impLeft' on goal 99 (script from line 66) 
626894     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 17: 'tryclose branch' on goal 100 (script from line 67) 
627031     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 18: 'rule andLeft' on goal 101 (script from line 68) 
627031     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 19: 'rule andLeft' on goal 188 (script from line 69) 
627035     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 20: 'rule seqNPermDefLeft' on goal 189 (script from line 71) 
627036     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 21: 'instantiate var=iv with='v_x_0' occ=2' on goal 190 (script from line 72) 
627037     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 22: 'rule impLeft' on goal 191 (script from line 73) 
627039     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 23: 'tryclose branch' on goal 192 (script from line 74) 
627203     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 24: 'rule exLeft' on goal 193 (script from line 75) 
627205     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 25: 'rule andLeft' on goal 310 (script from line 76) 
627206     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 26: 'rule andLeft' on goal 311 (script from line 77) 
627207     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 27: 'instantiate hide var=iv with='v_y_0' occ=2' on goal 312 (script from line 79) 
627208     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 28: 'rule impLeft' on goal 313 (script from line 80) 
627210     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 29: 'tryclose branch' on goal 314 (script from line 81) 
627351     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 30: 'rule exLeft' on goal 315 (script from line 82) 
627352     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 31: 'rule andLeft' on goal 420 (script from line 83) 
627354     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 32: 'rule andLeft' on goal 421 (script from line 84) 
627355     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 33: 'instantiate var=iv with='jv_0' occ=1' on goal 422 (script from line 86) 
627356     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 34: 'rule impLeft' on goal 423 (script from line 87) 
627358     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 35: 'tryclose branch' on goal 424 (script from line 88) 
627366     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 36: 'rule andLeft' on goal 425 (script from line 89) 
627367     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 37: 'rule andLeft' on goal 434 (script from line 90) 
627369     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 38: 'rule castAdd formula='s_0[jv_0] = v_x_0' occ=0' on goal 435 (script from line 91) 
627370     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 39: 'instantiate hide var=iv with='jv_1' occ=1' on goal 436 (script from line 93) 
627372     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 40: 'rule impLeft' on goal 437 (script from line 94) 
627374     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 41: 'tryclose branch' on goal 438 (script from line 95) 
627384     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 42: 'rule andLeft' on goal 439 (script from line 96) 
627385     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 43: 'rule andLeft' on goal 448 (script from line 97) 
627386     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 44: 'rule castAdd formula='s_0[jv_1] = v_y_0' occ=0' on goal 449 (script from line 98) 
627386     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 45: 'instantiate var=iv  with='v_x_0'' on goal 450 (script from line 100) 
627388     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 46: 'rule impLeft' on goal 451 (script from line 101) 
627388     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 47: 'tryclose branch' on goal 452 (script from line 102) 
627580     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 48: 'instantiate var=iv  with='v_y_0'' on goal 453 (script from line 104) 
627582     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 49: 'rule impLeft' on goal 562 (script from line 105) 
627583     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 50: 'tryclose branch' on goal 563 (script from line 106) 
627759     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 51: 'cut 'v_x_0 = v_y_0'' on goal 564 (script from line 108) 
627760     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 52: 'instantiate hide var='v_r' with='seqSwap(s_0,v_x_0,jv_0)'' on goal 674 (script from line 110) 
627761     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 53: 'rule andRight' on goal 676 (script from line 112) 
627763     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 54: 'rule andRight' on goal 677 (script from line 113) 
627764     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 55: 'rule andRight' on goal 679 (script from line 114) 
627765     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 56: 'rule andRight' on goal 681 (script from line 115) 
627769     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 57: 'rule lenOfSwap' on goal 683 (script from line 116) 
627769     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 58: 'tryclose branch' on goal 685 (script from line 117) 
627775     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 59: 'rule seqNPermSwapNPerm' on goal 684 (script from line 119) 
627776     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 60: 'instantiate hide var='iv' with='v_x_0' occ=1' on goal 687 (script from line 120) 
627777     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 61: 'instantiate hide var='jv' with='jv_0'' on goal 688 (script from line 121) 
627778     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 62: 'rule impLeft' on goal 689 (script from line 122) 
627779     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 63: 'tryclose branch' on goal 690 (script from line 123) 
627900     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 64: 'tryclose branch' on goal 691 (script from line 124) 
627904     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 65: 'rule allRight' on goal 682 (script from line 126) 
627905     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 66: 'rule impRight' on goal 796 (script from line 127) 
627906     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 67: 'rule andLeft' on goal 797 (script from line 128) 
627907     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 68: 'instantiate var=iv with='v_iv_0'' on goal 798 (script from line 129) 
627908     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 69: 'rule impLeft' on goal 799 (script from line 130) 
627912     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 70: 'tryclose branch' on goal 800 (script from line 131) 
628049     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 71: 'rule getOfSwap' on goal 801 (script from line 132) 
628050     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 72: 'rule ifthenelse_negated' on goal 912 (script from line 133) 
628051     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 73: 'rule ifthenelse_split occ=0' on goal 913 (script from line 134) 
628053     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 74: 'rule andLeft' on goal 914 (script from line 135) 
628053     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 75: 'rule andLeft' on goal 916 (script from line 136) 
628054     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 76: 'rule andLeft' on goal 917 (script from line 137) 
628055     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 77: 'rule ifthenelse_split occ=0' on goal 918 (script from line 138) 
628056     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 78: 'tryclose branch' on goal 919 (script from line 139) 
628166     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 79: 'rule ifthenelse_split occ=0' on goal 920 (script from line 140) 
628168     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 80: 'tryclose branch' on goal 1011 (script from line 141) 
628293     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 81: 'tryclose branch' on goal 1012 (script from line 142) 
628298     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 82: 'tryclose branch' on goal 915 (script from line 143) 
628304     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 83: 'rule getOfSwap' on goal 680 (script from line 145) 
628305     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 84: 'rule ifthenelse_negated' on goal 1099 (script from line 146) 
628307     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 85: 'rule ifthenelse_split occ=0' on goal 1100 (script from line 147) 
628308     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 86: 'rule andLeft' on goal 1101 (script from line 148) 
628310     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 87: 'rule andLeft' on goal 1103 (script from line 149) 
628311     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 88: 'rule andLeft' on goal 1104 (script from line 150) 
628311     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 89: 'rule ifthenelse_split occ=0' on goal 1105 (script from line 151) 
628312     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 90: 'tryclose branch' on goal 1106 (script from line 152) 
628321     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 91: 'tryclose branch' on goal 1107 (script from line 153) 
628326     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 92: 'tryclose branch' on goal 1102 (script from line 154) 
628437     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 93: 'rule getOfSwap' on goal 678 (script from line 156) 
628439     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 94: 'rule ifthenelse_negated' on goal 1225 (script from line 157) 
628441     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 95: 'rule ifthenelse_split occ=0' on goal 1226 (script from line 158) 
628443     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 96: 'rule andLeft' on goal 1227 (script from line 159) 
628443     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 97: 'rule andLeft' on goal 1229 (script from line 160) 
628444     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 98: 'rule andLeft' on goal 1230 (script from line 161) 
628444     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 99: 'rule ifthenelse_split occ=0' on goal 1231 (script from line 162) 
628445     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 100: 'tryclose branch' on goal 1232 (script from line 163) 
628507     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 101: 'tryclose branch' on goal 1233 (script from line 164) 
628514     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 102: 'tryclose branch' on goal 1228 (script from line 165) 
628616     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 103: 'cut '(int)s_0[v_x_0] = (int)s_0[v_y_0]'' on goal 675 (script from line 168) 
628618     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 104: 'rule seqNPermInjective' on goal 1397 (script from line 169) 
628619     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 105: 'instantiate hide var=iv with='v_x_0'' on goal 1399 (script from line 170) 
628620     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 106: 'instantiate hide var=jv with='v_y_0'' on goal 1400 (script from line 171) 
628621     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 107: 'rule impLeft' on goal 1401 (script from line 172) 
628622     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 108: 'tryclose branch' on goal 1402 (script from line 173) 
628763     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 109: 'tryclose branch' on goal 1403 (script from line 174) 
628768     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 110: 'cut '(int)s_0[v_x_0] = v_x_0'' on goal 1398 (script from line 176) 
628770     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 111: 'instantiate hide var=v_r with='seqSwap(s_0,v_y_0,jv_1)'' on goal 1534 (script from line 178) 
628771     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 112: 'rule andRight' on goal 1536 (script from line 180) 
628773     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 113: 'rule andRight' on goal 1537 (script from line 181) 
628773     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 114: 'rule andRight' on goal 1539 (script from line 182) 
628774     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 115: 'rule andRight' on goal 1541 (script from line 183) 
628775     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 116: 'tryclose branch' on goal 1543 (script from line 184) 
628785     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 117: 'rule seqNPermSwapNPerm' on goal 1544 (script from line 186) 
628790     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 118: 'instantiate hide var=iv with='v_y_0'' on goal 1558 (script from line 187) 
628791     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 119: 'instantiate hide var=jv with='jv_1'' on goal 1559 (script from line 188) 
628792     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 120: 'tryclose branch' on goal 1560 (script from line 189) 
628904     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 121: 'rule allRight' on goal 1542 (script from line 191) 
628905     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 122: 'rule impRight' on goal 1667 (script from line 192) 
628907     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 123: 'rule andLeft' on goal 1668 (script from line 193) 
628907     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 124: 'instantiate var=iv with='v_iv_0'' on goal 1669 (script from line 194) 
628908     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 125: 'rule impLeft' on goal 1670 (script from line 195) 
628909     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 126: 'tryclose branch' on goal 1671 (script from line 196) 
629034     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 127: 'rule getOfSwap' on goal 1672 (script from line 197) 
629036     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 128: 'rule ifthenelse_negated' on goal 1786 (script from line 198) 
629037     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 129: 'rule ifthenelse_split occ=0' on goal 1787 (script from line 199) 
629038     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 130: 'rule andLeft' on goal 1788 (script from line 200) 
629039     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 131: 'rule andLeft' on goal 1790 (script from line 201) 
629040     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 132: 'rule andLeft' on goal 1791 (script from line 202) 
629040     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 133: 'rule ifthenelse_split occ=0' on goal 1792 (script from line 203) 
629041     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 134: 'tryclose branch' on goal 1793 (script from line 204) 
629137     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 135: 'rule ifthenelse_split occ=0' on goal 1794 (script from line 205) 
629139     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 136: 'tryclose branch' on goal 1885 (script from line 206) 
629238     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 137: 'instantiate var=iv with='v_y_0'' on goal 1886 (script from line 207) 
629239     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 138: 'rule impLeft' on goal 1968 (script from line 208) 
629240     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 139: 'tryclose branch' on goal 1969 (script from line 209) 
629246     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 140: 'tryclose branch' on goal 1970 (script from line 210) 
629251     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 141: 'tryclose branch' on goal 1789 (script from line 211) 
629257     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 142: 'tryclose branch' on goal 1540 (script from line 212) 
629424     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 143: 'rule getOfSwap' on goal 1538 (script from line 214) 
629425     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 144: 'rule ifthenelse_negated' on goal 2097 (script from line 215) 
629426     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 145: 'rule ifthenelse_split occ=0' on goal 2098 (script from line 216) 
629428     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 146: 'tryclose branch' on goal 2099 (script from line 217) 
629442     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 147: 'tryclose branch' on goal 2100 (script from line 218) 
629542     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 148: 'tryclose branch' on goal 1535 (script from line 220) 
633411     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 149: 'cut  '(int)s_0[v_y_0] = v_y_0'' on goal 1535 (script from line 223) 
633412     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 150: 'instantiate hide var=v_r with='seqSwap(s_0,v_x_0,jv_0)'' on goal 4266 (script from line 225) 
633415     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 151: 'rule andRight' on goal 4268 (script from line 227) 
633417     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 152: 'rule andRight' on goal 4269 (script from line 228) 
633418     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 153: 'rule andRight' on goal 4271 (script from line 229) 
633418     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 154: 'rule andRight' on goal 4273 (script from line 230) 
633419     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 155: 'tryclose branch' on goal 4275 (script from line 231) 
633427     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 156: 'rule seqNPermSwapNPerm' on goal 4276 (script from line 233) 
633428     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 157: 'instantiate hide var=iv with='v_x_0'' on goal 4287 (script from line 234) 
633429     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 158: 'instantiate hide var=jv with='jv_0'' on goal 4288 (script from line 235) 
633429     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 159: 'rule impLeft' on goal 4289 (script from line 236) 
633430     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 160: 'tryclose branch' on goal 4290 (script from line 237) 
633525     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 161: 'tryclose branch' on goal 4291 (script from line 238) 
633529     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 162: 'rule allRight' on goal 4274 (script from line 240) 
633530     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 163: 'rule impRight' on goal 4400 (script from line 241) 
633531     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 164: 'rule andLeft' on goal 4401 (script from line 242) 
633531     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 165: 'instantiate var=iv with='v_iv_0'' on goal 4402 (script from line 243) 
633532     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 166: 'rule impLeft' on goal 4403 (script from line 244) 
633533     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 167: 'tryclose branch' on goal 4404 (script from line 245) 
633630     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 168: 'rule getOfSwap' on goal 4405 (script from line 246) 
633631     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 169: 'rule ifthenelse_negated' on goal 4521 (script from line 247) 
633632     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 170: 'rule ifthenelse_split occ=0' on goal 4522 (script from line 248) 
633633     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 171: 'rule andLeft' on goal 4523 (script from line 249) 
633634     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 172: 'rule andLeft' on goal 4525 (script from line 250) 
633635     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 173: 'rule andLeft' on goal 4526 (script from line 251) 
633635     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 174: 'rule ifthenelse_split occ=0' on goal 4527 (script from line 252) 
633637     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 175: 'tryclose branch' on goal 4528 (script from line 253) 
633717     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 176: 'rule ifthenelse_split occ=0' on goal 4529 (script from line 254) 
633718     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 177: 'tryclose branch' on goal 4622 (script from line 255) 
633803     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 178: 'tryclose branch' on goal 4623 (script from line 256) 
633808     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 179: 'tryclose branch' on goal 4524 (script from line 257) 
633812     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 180: 'rule getOfSwap' on goal 4272 (script from line 259) 
633813     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 181: 'rule ifthenelse_negated' on goal 4713 (script from line 260) 
633814     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 182: 'rule ifthenelse_split occ=0' on goal 4714 (script from line 261) 
633815     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 183: 'tryclose branch' on goal 4715 (script from line 262) 
633826     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 184: 'tryclose branch' on goal 4716 (script from line 263) 
633916     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 185: 'rule getOfSwap' on goal 4270 (script from line 265) 
633917     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 186: 'rule ifthenelse_negated' on goal 4839 (script from line 266) 
633918     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 187: 'rule ifthenelse_split occ=0' on goal 4840 (script from line 267) 
633919     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 188: 'tryclose branch' on goal 4841 (script from line 268) 
633995     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 189: 'tryclose branch' on goal 4842 (script from line 269) 
634005     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 190: 'cut '(int)s_0[v_x_0]=v_y_0'' on goal 4267 (script from line 272) 
634005     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 191: 'instantiate hide var=v_r with='seqSwap(seqSwap(s_0,jv_0,v_x_0),jv_0,v_y_0)'' on goal 4948 (script from line 274) 
634006     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 192: 'rule andRight' on goal 4950 (script from line 276) 
634008     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 193: 'rule andRight' on goal 4951 (script from line 277) 
634008     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 194: 'rule andRight' on goal 4953 (script from line 278) 
634009     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 195: 'rule andRight' on goal 4955 (script from line 279) 
634009     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 196: 'tryclose branch' on goal 4957 (script from line 280) 
634021     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 197: 'rule seqNPermSwapNPerm' on goal 4958 (script from line 282) 
634022     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 198: 'instantiate hide var=iv with='jv_0'' on goal 4977 (script from line 283) 
634023     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 199: 'instantiate hide var=jv with='v_x_0'' on goal 4978 (script from line 284) 
634024     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 200: 'rule impLeft' on goal 4979 (script from line 285) 
634024     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 201: 'tryclose branch' on goal 4980 (script from line 286) 
634115     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 202: 'rule seqNPermSwapNPerm formula='seqNPerm(seqSwap(s_0, jv_0, v_x_0))'' on goal 4981 (script from line 287) 
634115     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 203: 'instantiate hide var=iv with='jv_0'' on goal 5093 (script from line 288) 
634117     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 204: 'instantiate hide var=jv with='v_y_0'' on goal 5094 (script from line 289) 
634117     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 205: 'rule impLeft' on goal 5095 (script from line 290) 
634118     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 206: 'tryclose branch' on goal 5096 (script from line 291) 
634211     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 207: 'tryclose branch' on goal 5097 (script from line 292) 
634215     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 208: 'rule allRight' on goal 4956 (script from line 294) 
634216     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 209: 'rule impRight' on goal 5212 (script from line 295) 
634217     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 210: 'rule andLeft' on goal 5213 (script from line 296) 
634218     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 211: 'instantiate var=iv with='v_iv_0'' on goal 5214 (script from line 299) 
634218     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 212: 'rule impLeft' on goal 5215 (script from line 300) 
634219     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 213: 'tryclose branch' on goal 5216 (script from line 301) 
634319     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 214: 'rule getOfSwap' on goal 5217 (script from line 303) 
634320     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 215: 'rule ifthenelse_negated' on goal 5337 (script from line 304) 
634321     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 216: 'rule ifthenelse_split occ=0' on goal 5338 (script from line 305) 
634322     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 217: 'rule andLeft' on goal 5339 (script from line 306) 
634323     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 218: 'rule andLeft' on goal 5341 (script from line 307) 
634323     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 219: 'rule andLeft' on goal 5342 (script from line 308) 
634323     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 220: 'rule ifthenelse_split occ=0' on goal 5343 (script from line 309) 
634324     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 221: 'rule getOfSwap' on goal 5344 (script from line 310) 
634325     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 222: 'rule ifthenelse_negated' on goal 5346 (script from line 311) 
634325     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 223: 'rule ifthenelse_split occ=0' on goal 5347 (script from line 312) 
634326     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 224: 'rule andLeft' on goal 5348 (script from line 313) 
634327     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 225: 'rule andLeft' on goal 5350 (script from line 314) 
634327     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 226: 'rule andLeft' on goal 5351 (script from line 315) 
634328     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 227: 'rule ifthenelse_split occ=0' on goal 5352 (script from line 316) 
634328     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 228: 'tryclose branch' on goal 5353 (script from line 317) 
634418     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 229: 'rule ifthenelse_split occ=0' on goal 5354 (script from line 318) 
634419     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 230: 'tryclose branch' on goal 5463 (script from line 319) 
634425     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 231: 'tryclose branch' on goal 5464 (script from line 320) 
634504     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 232: 'tryclose branch' on goal 5349 (script from line 321) 
634586     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 233: 'rule ifthenelse_split' on goal 5345 (script from line 323) 
634587     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 234: 'rule getOfSwap' on goal 5660 (script from line 324) 
634588     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 235: 'rule ifthenelse_negated' on goal 5662 (script from line 325) 
634588     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 236: 'rule ifthenelse_split occ=0' on goal 5663 (script from line 326) 
634589     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 237: 'rule andLeft' on goal 5664 (script from line 327) 
634590     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 238: 'rule andLeft' on goal 5666 (script from line 328) 
634590     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 239: 'rule andLeft' on goal 5667 (script from line 329) 
634590     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 240: 'rule ifthenelse_split occ=0' on goal 5668 (script from line 330) 
634591     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 241: 'tryclose branch' on goal 5669 (script from line 331) 
634678     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 242: 'tryclose branch' on goal 5670 (script from line 332) 
634684     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 243: 'tryclose branch' on goal 5665 (script from line 333) 
634776     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 244: 'rule getOfSwap' on goal 5661 (script from line 335) 
634777     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 245: 'rule ifthenelse_negated' on goal 5887 (script from line 336) 
634778     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 246: 'rule ifthenelse_split occ=0' on goal 5888 (script from line 337) 
634779     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 247: 'rule andLeft' on goal 5889 (script from line 338) 
634779     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 248: 'rule andLeft' on goal 5891 (script from line 339) 
634780     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 249: 'rule andLeft' on goal 5892 (script from line 340) 
634780     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 250: 'rule ifthenelse_split occ=0' on goal 5893 (script from line 341) 
634781     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 251: 'tryclose branch' on goal 5894 (script from line 342) 
634786     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 252: 'rule ifthenelse_split occ=0' on goal 5895 (script from line 343) 
634787     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 253: 'tryclose branch' on goal 5897 (script from line 344) 
634922     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 254: 'tryclose branch' on goal 5898 (script from line 345) 
634927     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 255: 'tryclose branch' on goal 5890 (script from line 346) 
634933     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 256: 'tryclose branch' on goal 5340 (script from line 347) 
635034     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 257: 'rule getOfSwap' on goal 4954 (script from line 349) 
635035     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 258: 'rule ifthenelse_negated' on goal 6115 (script from line 350) 
635036     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 259: 'rule ifthenelse_split occ=0' on goal 6116 (script from line 351) 
635037     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 260: 'rule andLeft' on goal 6117 (script from line 352) 
635037     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 261: 'rule andLeft' on goal 6119 (script from line 353) 
635038     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 262: 'rule andLeft' on goal 6120 (script from line 354) 
635038     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 263: 'rule ifthenelse_split occ=0' on goal 6121 (script from line 355) 
635039     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 264: 'tryclose branch' on goal 6122 (script from line 356) 
635094     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 265: 'rule ifthenelse_split occ=0' on goal 6123 (script from line 357) 
635096     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 266: 'rule getOfSwap' on goal 6193 (script from line 358) 
635096     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 267: 'rule ifthenelse_negated' on goal 6195 (script from line 359) 
635097     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 268: 'rule ifthenelse_split occ=0' on goal 6196 (script from line 360) 
635098     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 269: 'tryclose branch' on goal 6197 (script from line 361) 
635104     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 270: 'tryclose branch' on goal 6198 (script from line 362) 
635109     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 271: 'tryclose branch' on goal 6194 (script from line 363) 
635225     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 272: 'tryclose branch' on goal 6118 (script from line 364) 
635315     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 273: 'rule getOfSwap' on goal 4952 (script from line 366) 
635315     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 274: 'rule ifthenelse_negated' on goal 6456 (script from line 367) 
635316     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 275: 'rule ifthenelse_split occ=0' on goal 6457 (script from line 368) 
635317     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 276: 'tryclose branch' on goal 6458 (script from line 369) 
635486     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 277: 'tryclose branch' on goal 6459 (script from line 370) 
635575     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 278: 'cut 'int::seqGet(s_0, v_y_0)=v_x_0'' on goal 4949 (script from line 374) 
635576     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 279: 'tryclose branch' on goal 6735 (script from line 377) 
638665     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 280: 'rule seqNPermSwapNPerm' on goal 6735 (script from line 379) 
638670     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 281: 'instantiate hide var=iv with='jv_1'' on goal 8783 (script from line 380) 
638671     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 282: 'instantiate hide var=jv with='v_y_0'' on goal 8784 (script from line 381) 
638671     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 283: 'rule impLeft' on goal 8785 (script from line 382) 
638745     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 284: 'tryclose branch' on goal 8786 (script from line 383) 
638860     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 285: 'rule seqNPermSwapNPerm formula='seqNPerm(seqSwap(s_0,jv_1,v_y_0))'' on goal 8787 (script from line 384) 
638861     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 286: 'instantiate hide var=iv with='jv_1'' on goal 8909 (script from line 385) 
638862     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 287: 'instantiate hide var=jv with='v_x_0'' on goal 8910 (script from line 386) 
638863     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 288: 'rule impLeft' on goal 8911 (script from line 387) 
638864     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 289: 'tryclose branch' on goal 8912 (script from line 388) 
638970     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 290: 'tryclose branch' on goal 8913 (script from line 389) 
642024     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 291: 'tryclose branch' on goal 6736 (script from line 396) 
645290     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 292: 'rule seqNPermSwapNPerm formula='seqNPerm(s_0)'' on goal 6736 (script from line 398) 
645294     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 293: 'instantiate hide var=iv with='v_x_0'' on goal 12633 (script from line 399) 
645294     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 294: 'instantiate hide var=jv with='jv_0'' on goal 12634 (script from line 400) 
645295     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 295: 'rule impLeft' on goal 12635 (script from line 401) 
645296     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 296: 'tryclose branch' on goal 12636 (script from line 402) 
645409     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 297: 'rule seqNPermSwapNPerm formula='seqNPerm(seqSwap(s_0,v_x_0,jv_0))'' on goal 12637 (script from line 403) 
645410     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 298: 'instantiate hide var=iv with='v_y_0'' on goal 12757 (script from line 404) 
645411     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 299: 'instantiate hide var=jv with='jv_1'' on goal 12758 (script from line 405) 
645412     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 300: 'instantiate hide var=v_r with='seqSwap(seqSwap(s_0, v_x_0, jv_0), v_y_0, jv_1)' ...' on goal 12759 (script from line 406) 
645412     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 301: 'tryclose branch' on goal 12760 (script from line 407) 
646598     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm2/Taclet_schiffl_thm_1.proof 
646598     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 113.4ns 
646603     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
649030     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.43s 
649030     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: schiffl_thm_1 
649840     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: schiffl_thm_1 
649841     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 6.7ns 
649841     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 1: 'macro split-prop' on goal 0 (script from line 50) 
649847     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 2: 'rule schiffl_lemma_2 formula='seqPerm(f_s, f_t)'' on goal 10 (script from line 51) 
649856     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 3: 'instantiate hide var=x with='f_x'' on goal 11 (script from line 52) 
649858     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 4: 'instantiate hide var=y with='f_y'' on goal 12 (script from line 53) 
649860     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 5: 'rule impLeft' on goal 13 (script from line 54) 
649861     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 6: 'tryclose branch' on goal 14 (script from line 55) 
649865     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 7: 'rule exLeft' on goal 15 (script from line 56) 
649865     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 8: 'macro split-prop' on goal 23 (script from line 57) 
649869     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 9: 'rule seqPermDef occ=1' on goal 27 (script from line 58) 
649869     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 10: 'rule andRight' on goal 28 (script from line 59) 
649871     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 11: 'tryclose branch' on goal 29 (script from line 60) 
649879     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 12: 'instantiate hide var=s with='r_0'' on goal 30 (script from line 61) 
649880     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 13: 'rule andRight' on goal 46 (script from line 62) 
649881     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 14: 'tryclose branch' on goal 47 (script from line 63) 
649925     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 15: 'rule allRight' on goal 48 (script from line 64) 
649926     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 16: 'rule impRight' on goal 119 (script from line 65) 
649927     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 17: 'instantiate hide var=iv with='iv_0'' on goal 120 (script from line 66) 
649927     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 18: 'rule impLeft' on goal 121 (script from line 67) 
649927     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 19: 'tryclose branch' on goal 122 (script from line 68) 
649991     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 20: 'rule andLeft' on goal 123 (script from line 69) 
649991     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 21: 'rule seqNPermRange' on goal 203 (script from line 70) 
649992     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 22: 'instantiate hide var=iv with='iv_0'' on goal 204 (script from line 71) 
649993     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 23: 'rule impLeft' on goal 205 (script from line 72) 
649993     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 24: 'tryclose branch' on goal 206 (script from line 73) 
649997     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 25: 'rule andLeft' on goal 207 (script from line 74) 
649997     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 26: 'rule andLeft' on goal 215 (script from line 75) 
649997     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 27: 'rule seqNPermRange' on goal 216 (script from line 76) 
649998     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 28: 'instantiate hide var=iv with='f_x'' on goal 217 (script from line 77) 
649998     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 29: 'rule impLeft' on goal 218 (script from line 78) 
649999     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 30: 'tryclose branch' on goal 219 (script from line 79) 
650081     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 31: 'rule andLeft' on goal 220 (script from line 80) 
650082     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 32: 'rule andLeft' on goal 311 (script from line 81) 
650082     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 33: 'rule seqNPermRange' on goal 312 (script from line 82) 
650083     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 34: 'instantiate hide var=iv with='f_y'' on goal 313 (script from line 83) 
650084     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 35: 'rule impLeft' on goal 314 (script from line 84) 
650085     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 36: 'tryclose branch' on goal 315 (script from line 85) 
650170     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 37: 'rule andLeft' on goal 316 (script from line 86) 
650171     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 38: 'rule andLeft' on goal 410 (script from line 87) 
650171     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 39: 'rule getOfSeqDef occ=0' on goal 411 (script from line 88) 
650172     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 40: 'rule getOfSeqDef' on goal 412 (script from line 89) 
650172     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 41: 'rule ifthenelse_split occ=0' on goal 413 (script from line 90) 
650173     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 42: 'rule andLeft occ=0' on goal 414 (script from line 91) 
650173     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 43: 'rule sub_zero_2 occ=0' on goal 416 (script from line 92) 
650174     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 44: 'rule ifthenelse_split occ=2' on goal 417 (script from line 93) 
650175     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 45: 'rule andLeft' on goal 418 (script from line 94) 
650175     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 46: 'rule sub_zero_2 occ=0' on goal 420 (script from line 95) 
650176     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 47: 'rule add_zero_right occ=0' on goal 421 (script from line 96) 
650176     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 48: 'rule add_zero_right occ=0' on goal 422 (script from line 97) 
650177     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 49: 'rule add_zero_right occ=0' on goal 423 (script from line 98) 
650177     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 50: 'rule add_zero_right occ=0' on goal 424 (script from line 99) 
650178     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 51: 'rule add_zero_right occ=0' on goal 425 (script from line 100) 
650178     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 52: 'rule add_zero_right occ=0' on goal 426 (script from line 101) 
650179     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 53: 'rule ifthenelse_split occ=0' on goal 427 (script from line 102) 
650179     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 54: 'rule ifthenelse_split occ=0' on goal 428 (script from line 103) 
650180     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 55: 'tryclose branch' on goal 430 (script from line 104) 
650183     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 56: 'tryclose branch' on goal 431 (script from line 105) 
650219     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 57: 'rule ifthenelse_split occ=0' on goal 429 (script from line 106) 
650220     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 58: 'tryclose branch' on goal 473 (script from line 107) 
650277     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 59: 'rule ifthenelse_split occ=0' on goal 474 (script from line 108) 
650278     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 60: 'rule seqNPermInjective' on goal 541 (script from line 109) 
650279     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 61: 'instantiate hide var=iv with='iv_0'' on goal 543 (script from line 110) 
650280     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 62: 'instantiate hide var=jv with='f_y'' on goal 544 (script from line 111) 
650281     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 63: 'rule impLeft' on goal 545 (script from line 112) 
650282     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 64: 'tryclose branch' on goal 546 (script from line 113) 
650334     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 65: 'tryclose branch' on goal 547 (script from line 114) 
650336     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 66: 'rule ifthenelse_split occ=0' on goal 542 (script from line 115) 
650337     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 67: 'rule seqNPermInjective' on goal 606 (script from line 116) 
650338     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 68: 'instantiate hide var=iv with='iv_0'' on goal 608 (script from line 117) 
650339     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 69: 'instantiate hide var=jv with='f_x'' on goal 609 (script from line 118) 
650340     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 70: 'rule impLeft' on goal 610 (script from line 119) 
650341     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 71: 'tryclose branch' on goal 611 (script from line 120) 
650390     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 72: 'tryclose branch' on goal 612 (script from line 121) 
650392     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 73: 'tryclose branch' on goal 607 (script from line 122) 
650395     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 74: 'tryclose branch' on goal 419 (script from line 123) 
650446     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 75: 'tryclose branch' on goal 415 (script from line 124) 
650499     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_eqSameSeq.proof 
650500     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 252.6ns 
650500     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
652888     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.39s 
652888     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: eqSameSeq 
653707     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: eqSameSeq 
653722     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 12.41ms

Standard error

ANTLR Tool version 4.12.0 used for code generation does not match the current runtime version 4.13.0
ANTLR Tool version 4.12.0 used for code generation does not match the current runtime version 4.13.0
ANTLR Tool version 4.12.0 used for code generation does not match the current runtime version 4.13.0
ANTLR Tool version 4.12.0 used for code generation does not match the current runtime version 4.13.0