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

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

tests
0

failures
0

ignored
13m54.31s

duration
100%

successful

Tests

Test Method name Duration Result
powPositive data()[100] 4.004s passed
powPositiveConcrete data()[101] 4.077s passed
powGeq1Concrete data()[102] 4.067s passed
pow2InIntLower data()[103] 4.029s passed
pow2InIntUpper data()[104] 4.018s passed
logSelfConcrete data()[105] 4.005s passed
log1Concrete data()[106] 3.982s passed
logProduct data()[107] 4.017s passed
logTimesBaseConcrete data()[108] 4.032s passed
logProdIdentity data()[109] 4.030s passed
moduloByteIsInByte data()[10] 4.029s passed
logProdIdentityConcrete data()[110] 3.993s passed
logPowIdentity data()[111] 4.054s passed
logPowIdentityConcrete data()[112] 4.037s passed
logPositive data()[113] 4.091s passed
logPositiveConcrete data()[114] 4.068s passed
logMono data()[115] 4.051s passed
logMonoConcrete data()[116] 4.060s passed
powLogLess data()[117] 4.024s passed
powLogMore2 data()[118] 4.065s passed
logLessThanPow data()[119] 3.988s passed
moduloCharIsInChar data()[11] 3.996s passed
logLessThanPowConcrete data()[120] 4.032s passed
logSqueeze data()[121] 4.072s passed
ifthenelse_equals data()[122] 3.967s passed
ifthenelse_equals_1 data()[123] 4.018s passed
ifthenelse_equals_2 data()[124] 3.987s passed
disjointWithSingleton1 data()[125] 4.057s passed
disjointWithSingleton2 data()[126] 4.106s passed
disjointArrayRanges data()[127] 4.144s passed
disjointArrayRangeAllFields1 data()[128] 4.270s passed
disjointArrayRangeAllFields2 data()[129] 4.268s passed
div_unique1 data()[12] 4.301s passed
seqSelfDefinition data()[130] 4.261s passed
seqOutsideValue data()[131] 4.047s passed
castedGetAny data()[132] 4.039s passed
seqGetAlphaCast data()[133] 4.140s passed
getOfSeqSingleton data()[134] 4.009s passed
getOfSeqSingletonConcrete data()[135] 4.059s passed
getOfSeqConcat data()[136] 4.014s passed
getOfSeqSub data()[137] 4.019s passed
getOfSeqReverse data()[138] 4.096s passed
lenOfSeqEmpty data()[139] 3.999s passed
div_unique2 data()[13] 4.153s passed
lenOfSeqSingleton data()[140] 4.018s passed
lenOfSeqConcat data()[141] 4.021s passed
lenOfSeqSub data()[142] 3.992s passed
lenOfSeqReverse data()[143] 4.107s passed
equalityToSeqGetAndSeqLenLeft data()[144] 3.972s passed
equalityToSeqGetAndSeqLenRight data()[145] 4.015s passed
getOfSeqSingletonEQ data()[146] 4.036s passed
getOfSeqConcatEQ data()[147] 4.217s passed
getOfSeqSubEQ data()[148] 4.146s passed
getOfSeqReverseEQ data()[149] 4.031s passed
div_exists data()[14] 4.248s passed
lenOfSeqEmptyEQ data()[150] 4.099s passed
lenOfSeqSingletonEQ data()[151] 4.115s passed
lenOfSeqConcatEQ data()[152] 4.095s passed
lenOfSeqSubEQ data()[153] 4.121s passed
lenOfSeqReverseEQ data()[154] 4.096s passed
getOfSeqDefEQ data()[155] 4.074s passed
lenOfSeqDefEQ data()[156] 4.089s passed
seqConcatWithSeqEmpty1 data()[157] 4.082s passed
seqConcatWithSeqEmpty2 data()[158] 4.015s passed
seqReverseOfSeqEmpty data()[159] 4.079s passed
div_one data()[15] 4.075s passed
subSeqComplete data()[160] 4.035s passed
subSeqTailR data()[161] 3.988s passed
subSeqTailL data()[162] 3.997s passed
subSeqTailEQR data()[163] 3.992s passed
subSeqTailEQL data()[164] 3.970s passed
seqDef_split data()[165] 4.037s passed
seqDef_induction_upper data()[166] 3.986s passed
seqDef_induction_upper_concrete data()[167] 4.021s passed
seqDef_induction_lower data()[168] 4.127s passed
seqDef_induction_lower_concrete data()[169] 4.069s passed
jdiv_one data()[16] 4.146s passed
seqDef_split_in_three data()[170] 4.179s passed
seqDef_empty data()[171] 4.126s passed
seqDef_one_summand data()[172] 4.088s passed
seqDef_lower_equals_upper data()[173] 4.085s passed
seqDefOfSeq data()[174] 4.076s passed
seqSelfDefinitionEQ2 data()[175] 4.112s passed
indexOfSeqSingleton data()[176] 4.048s passed
indexOfSeqConcatFirst data()[177] 4.157s passed
indexOfSeqConcatSecond data()[178] 4.016s passed
indexOfSeqSub data()[179] 4.052s passed
div_zero data()[17] 4.158s passed
lenOfArray2seq data()[180] 4.092s passed
getAnyOfArray2seq data()[181] 3.984s passed
getOfArray2seq data()[182] 4.109s passed
getAnyOfNPermInv data()[183] 4.007s passed
seqNPermRange data()[184] 4.074s passed
seqPermTrans data()[185] 4.128s passed
seqPermRefl data()[186] 4.127s passed
seqPermSplit data()[187] 4.054s passed
seqNPermRight data()[188] 4.137s passed
seqPermFromSwap data()[189] 4.095s passed
divResZero1 data()[18] 4.162s passed
seqPermTransAlt0 data()[190] 4.027s passed
seqPermTransAlt1 data()[191] 4.026s passed
seqPermTransAlt2 data()[192] 3.991s passed
seqPermTransAlt3 data()[193] 4.054s passed
seqPermForall data()[194] 4.214s passed
seqPermExists data()[195] 4.271s passed
schiffl_lemma_2 data()[196] 29.552s passed
schiffl_thm_1 data()[197] 5.151s passed
eqSameSeq data()[198] 4.339s passed
divResZero2 data()[19] 4.162s passed
eqTermCut data()[1] 5.246s passed
divResOne1 data()[20] 4.098s passed
divResOne2 data()[21] 4.251s passed
div_cancel1 data()[22] 4.051s passed
div_cancel2 data()[23] 3.998s passed
divAddMultDenom data()[24] 4.136s passed
divMinus data()[25] 3.984s passed
divMinusDenom data()[26] 4.071s passed
divLeastDPos data()[27] 3.977s passed
divLeastDNeg data()[28] 3.980s passed
divGreatestDPos data()[29] 3.916s passed
equivAllRight data()[2] 4.638s passed
divGreatestDNeg data()[30] 3.840s passed
divIncreasingPos data()[31] 3.962s passed
divIncreasingNeg data()[32] 3.928s passed
jdiv_zero data()[33] 3.890s passed
jdivPulloutMinusNum data()[34] 4.022s passed
jdivPulloutMinusDenom data()[35] 4.019s passed
jdiv_uniquePosPos data()[36] 4.057s passed
jdiv_uniquePosNeg data()[37] 4.003s passed
jdiv_uniqueNegPos data()[38] 3.856s passed
jdiv_uniqueNegNeg data()[39] 4.049s passed
irrflConcrete1 data()[3] 4.371s passed
jdivMultDenom1 data()[40] 3.970s passed
jdivMultDenom2 data()[41] 3.953s passed
mod_geZero data()[42] 3.984s passed
mod_lessDenom data()[43] 4.032s passed
jmod_NumPos data()[44] 4.197s passed
jmod_NumNeg data()[45] 4.100s passed
jmod_geZero data()[46] 4.030s passed
jmodNumZero data()[47] 4.156s passed
jmod_pulloutminusNum data()[48] 4.121s passed
jmod_pulloutminusDenom data()[49] 4.076s passed
irrflConcrete2 data()[4] 4.092s passed
jmodUnique1 data()[50] 4.330s passed
jmodUnique2 data()[51] 4.166s passed
intDivRem data()[52] 4.038s passed
jmodjmod data()[53] 4.045s passed
jmodDivisible data()[54] 4.149s passed
jmodDivisibleRep data()[55] 4.111s passed
jdivAddMultDenom data()[56] 4.241s passed
jmodAltZero data()[57] 4.043s passed
jmodAddMultDenomZero data()[58] 4.004s passed
polyDiv_zero data()[59] 4.079s passed
cancel_gtPos data()[5] 4.264s passed
polyMod_ltdivDenom data()[60] 4.098s passed
bsum_empty data()[61] 4.011s passed
bsum_induction_upper data()[62] 4.083s passed
bsum_induction_lower data()[63] 4.049s passed
bsum_num_of_bounds data()[64] 4.040s passed
bsum_num_of_bounds2 data()[65] 4.078s passed
bsum_induction_upper2 data()[66] 4.096s passed
bsum_induction_upper_concrete data()[67] 3.955s passed
bsum_induction_upper_concrete_2 data()[68] 3.986s passed
bsum_induction_upper2_concrete data()[69] 4.064s passed
cancel_gtNeg data()[6] 4.165s passed
bsum_induction_lower_concrete data()[70] 4.039s passed
bsum_induction_lower2 data()[71] 4.084s passed
bsum_induction_lower2_concrete data()[72] 4.061s passed
bsum_positive data()[73] 4.169s passed
bsum_upper_bound data()[74] 4.149s passed
bsum_lower_bound data()[75] 4.221s passed
bsum_positive_lower_bound_element data()[76] 4.138s passed
bsum_sub_same_index data()[77] 4.090s passed
bsum_less_same_index data()[78] 4.127s passed
bsum_equal_except_one_index data()[79] 4.035s passed
moduloIntIsInInt data()[7] 4.127s passed
bsum_num_of_is_max data()[80] 4.079s passed
bsum_num_of_is_max2 data()[81] 4.052s passed
bsum_num_of_is_max3 data()[82] 4.047s passed
bsum_num_of_is_max4 data()[83] 4.108s passed
bsum_num_of_lt_max data()[84] 4.113s passed
bsum_num_of_lt_max2 data()[85] 4.086s passed
bsum_num_of_lt_max3 data()[86] 4.007s passed
bsum_num_of_lt_max4 data()[87] 4.028s passed
bsum_num_of_gt0 data()[88] 4.073s passed
bsum_num_of_gt0_alt data()[89] 4.083s passed
moduloLongIsInLong data()[8] 3.977s passed
bsum_add_concrete data()[90] 4.037s passed
bprod_all_positive data()[91] 4.028s passed
bprod_split data()[92] 4.018s passed
powConcrete0 data()[93] 4.042s passed
powConcrete1 data()[94] 4.033s passed
powSplitFactor data()[95] 4.040s passed
powAdd data()[96] 4.031s passed
powMono data()[97] 4.081s passed
powMonoConcrete data()[98] 4.101s passed
powMonoConcreteRight data()[99] 4.026s passed
moduloShortIsInShort data()[9] 4.095s passed

Standard output

791        INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src/test/resources/testcase/dummyTrue.key 
816        DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 9.86ms 
1119       INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
1141       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)

2546       DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for Meta 
2549       DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for Meta 
2555       DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for Meta 
2555       DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for Meta 
4467       DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for JavaBigintExpression 
11378      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 10.26s 
11474      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof dummyTrue.key 
11526      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 43.2ns 
11542      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/firstOrder/Taclet_eqTermCut.proof 
11543      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 269ns 
11553      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
15543      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.99s 
15546      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: eqTermCut 
16726      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: eqTermCut 
16768      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 28.08ms 
16795      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/firstOrder/Taclet_equivAllRight.proof 
16795      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 215.4ns 
16801      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
20290      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.49s 
20290      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: equivAllRight 
21411      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: equivAllRight 
21427      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 11.54ms 
21431      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_irrflConcrete1.proof 
21432      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 411ns 
21434      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
24695      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.26s 
24696      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: irrflConcrete1 
25782      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: irrflConcrete1 
25797      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 6.44ms 
25803      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_irrflConcrete2.proof 
25804      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 170.5ns 
25806      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
28900      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.09s 
28900      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: irrflConcrete2 
29887      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: irrflConcrete2 
29894      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.43ms 
29897      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_cancel_gtPos.proof 
29898      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 430.6ns 
29899      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
33079      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.18s 
33080      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: cancel_gtPos 
34105      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: cancel_gtPos 
34158      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 48.18ms 
34162      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_cancel_gtNeg.proof 
34162      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 416.7ns 
34164      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
37285      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.12s 
37287      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: cancel_gtNeg 
38294      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: cancel_gtNeg 
38325      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 22.16ms 
38327      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intRulesIgnoringOF/Taclet_moduloIntIsInInt.proof 
38327      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 113.4ns 
38328      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
41434      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.11s 
41435      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: moduloIntIsInInt 
42417      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: moduloIntIsInInt 
42451      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.6ms 
42454      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intRulesIgnoringOF/Taclet_moduloLongIsInLong.proof 
42454      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 143ns 
42455      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
45441      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.99s 
45441      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: moduloLongIsInLong 
46426      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: moduloLongIsInLong 
46429      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 663.9ns 
46432      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intRulesIgnoringOF/Taclet_moduloShortIsInShort.proof 
46432      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 400.1ns 
46436      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
49522      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.09s 
49522      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: moduloShortIsInShort 
50521      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: moduloShortIsInShort 
50525      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 740.3ns 
50528      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intRulesIgnoringOF/Taclet_moduloByteIsInByte.proof 
50529      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 699.3ns 
50530      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
53569      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.04s 
53570      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: moduloByteIsInByte 
54551      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: moduloByteIsInByte 
54555      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 684ns 
54557      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intRulesIgnoringOF/Taclet_moduloCharIsInChar.proof 
54557      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 127.7ns 
54558      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
57546      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.99s 
57547      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: moduloCharIsInChar 
58546      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: moduloCharIsInChar 
58549      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 764.11ns 
58553      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_div_unique1.proof 
58553      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 443.9ns 
58565      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
61785      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.22s 
61785      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: div_unique1 
62746      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: div_unique1 
62845      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 94.27ms 
62860      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_div_unique2.proof 
62861      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 518.9ns 
62862      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
65972      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.11s 
65972      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: div_unique2 
66967      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: div_unique2 
67008      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 36.46ms 
67013      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_div_exists.proof 
67019      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 6.37ms 
67021      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
70107      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.09s 
70108      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: div_exists 
71100      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: div_exists 
71258      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 147.2ms 
71260      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_div_one.proof 
71260      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 130ns 
71261      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
74335      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.07s 
74336      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: div_one 
75324      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: div_one 
75332      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.63ms 
75335      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdiv_one.proof 
75335      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 169.1ns 
75336      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
78442      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.11s 
78444      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdiv_one 
79474      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdiv_one 
79479      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.68ms 
79482      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_div_zero.proof 
79483      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 524.9ns 
79484      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
82575      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.09s 
82576      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: div_zero 
83579      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: div_zero 
83638      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 52.67ms 
83645      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divResZero1.proof 
83645      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 360.5ns 
83647      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
86806      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.16s 
86807      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divResZero1 
87788      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divResZero1 
87804      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 11.8ms 
87807      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divResZero2.proof 
87807      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 376ns 
87809      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
90969      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.16s 
90969      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divResZero2 
91949      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divResZero2 
91966      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 12.84ms 
91968      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divResOne1.proof 
91968      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 127.7ns 
91969      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
95058      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.09s 
95058      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divResOne1 
96045      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divResOne1 
96063      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 14.08ms 
96066      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divResOne2.proof 
96067      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 387.9ns 
96068      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
99240      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.17s 
99241      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divResOne2 
100296     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divResOne2 
100315     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 15.01ms 
100317     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_div_cancel1.proof 
100317     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 119ns 
100319     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
103394     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.07s 
103394     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: div_cancel1 
104342     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: div_cancel1 
104366     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 19.6ms 
104368     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_div_cancel2.proof 
104368     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 110.3ns 
104369     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
107382     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.01s 
107382     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: div_cancel2 
108359     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: div_cancel2 
108364     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.98ms 
108366     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divAddMultDenom.proof 
108367     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 366.4ns 
108368     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
111489     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.12s 
111490     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divAddMultDenom 
112450     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divAddMultDenom 
112499     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 42.28ms 
112503     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divMinus.proof 
112504     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 981.71ns 
112506     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
115437     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.93s 
115438     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divMinus 
116401     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divMinus 
116484     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 74.62ms 
116488     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divMinusDenom.proof 
116488     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 399.2ns 
116490     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
119489     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3s 
119489     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divMinusDenom 
120497     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divMinusDenom 
120557     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 52.78ms 
120559     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divLeastDPos.proof 
120559     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 104.5ns 
120560     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
123560     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3s 
123560     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divLeastDPos 
124525     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divLeastDPos 
124535     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 6.79ms 
124536     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divLeastDNeg.proof 
124536     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 102.9ns 
124537     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
127507     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.97s 
127507     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divLeastDNeg 
128485     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divLeastDNeg 
128513     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 24.91ms 
128523     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divGreatestDPos.proof 
128523     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 346.4ns 
128524     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
131526     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3s 
131527     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divGreatestDPos 
132423     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divGreatestDPos 
132437     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 10.76ms 
132438     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divGreatestDNeg.proof 
132438     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 85.1ns 
132439     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
135340     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.9s 
135341     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divGreatestDNeg 
136267     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divGreatestDNeg 
136276     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 6.54ms 
136277     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divIncreasingPos.proof 
136277     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 100.5ns 
136278     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
139214     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.94s 
139215     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divIncreasingPos 
140227     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divIncreasingPos 
140238     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 8.14ms 
140241     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divIncreasingNeg.proof 
140241     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 387.1ns 
140243     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
143210     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.97s 
143210     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divIncreasingNeg 
144157     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divIncreasingNeg 
144166     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 6.47ms 
144168     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdiv_zero.proof 
144168     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 103.3ns 
144169     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
147108     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.94s 
147109     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdiv_zero 
148049     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdiv_zero 
148056     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.39ms 
148058     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdivPulloutMinusNum.proof 
148058     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 139.4ns 
148059     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
151126     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.07s 
151126     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdivPulloutMinusNum 
152061     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdivPulloutMinusNum 
152078     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 12.84ms 
152079     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdivPulloutMinusDenom.proof 
152080     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 133.8ns 
152081     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
155050     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.97s 
155052     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdivPulloutMinusDenom 
156003     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdivPulloutMinusDenom 
156092     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 74.91ms 
156099     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdiv_uniquePosPos.proof 
156100     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 218.6ns 
156103     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
159159     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.06s 
159159     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdiv_uniquePosPos 
160132     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdiv_uniquePosPos 
160155     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 19.2ms 
160157     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdiv_uniquePosNeg.proof 
160157     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 94.2ns 
160158     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
163160     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3s 
163161     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdiv_uniquePosNeg 
164127     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdiv_uniquePosNeg 
164158     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 26.79ms 
164161     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdiv_uniqueNegPos.proof 
164161     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 283.8ns 
164162     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
167082     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.92s 
167083     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdiv_uniqueNegPos 
167993     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdiv_uniqueNegPos 
168014     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 17.84ms 
168016     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdiv_uniqueNegNeg.proof 
168016     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 89.1ns 
168017     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
171077     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.06s 
171077     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdiv_uniqueNegNeg 
172041     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdiv_uniqueNegNeg 
172063     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 18.43ms 
172065     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdivMultDenom1.proof 
172065     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 98ns 
172066     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
175031     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.97s 
175032     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdivMultDenom1 
175986     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdivMultDenom1 
176033     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 41.78ms 
176035     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdivMultDenom2.proof 
176035     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 74.4ns 
176036     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
178981     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.94s 
178981     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdivMultDenom2 
179979     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdivMultDenom2 
179986     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 5.02ms 
179991     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_mod_geZero.proof 
179993     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 2.14ms 
179995     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
183025     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.03s 
183025     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: mod_geZero 
183964     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: mod_geZero 
183970     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.88ms 
183972     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_mod_lessDenom.proof 
183972     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 110ns 
183973     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
186982     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.01s 
186983     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: mod_lessDenom 
187994     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: mod_lessDenom 
188004     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 7.3ms 
188005     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmod_NumPos.proof 
188005     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 104.9ns 
188006     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
191194     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.19s 
191195     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmod_NumPos 
192189     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmod_NumPos 
192200     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 8.71ms 
192202     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmod_NumNeg.proof 
192202     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 75.5ns 
192203     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
195291     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.09s 
195291     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmod_NumNeg 
196276     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmod_NumNeg 
196300     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 20.27ms 
196302     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmod_geZero.proof 
196302     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 92.1ns 
196303     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
199326     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.02s 
199327     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmod_geZero 
200320     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmod_geZero 
200330     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 7.21ms 
200332     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmodNumZero.proof 
200332     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 100.1ns 
200333     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
203430     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.1s 
203430     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmodNumZero 
204482     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmodNumZero 
204486     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.88ms 
204492     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmod_pulloutminusNum.proof 
204493     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 444ns 
204496     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
207618     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.12s 
207619     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmod_pulloutminusNum 
208602     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmod_pulloutminusNum 
208607     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.41ms 
208609     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmod_pulloutminusDenom.proof 
208609     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 84.3ns 
208610     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
211724     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.11s 
211725     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmod_pulloutminusDenom 
212678     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmod_pulloutminusDenom 
212683     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.69ms 
212685     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmodUnique1.proof 
212685     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 273ns 
212687     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
215909     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.22s 
215909     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmodUnique1 
216908     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmodUnique1 
217012     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 93.76ms 
217015     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmodUnique2.proof 
217015     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 340.5ns 
217017     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
220068     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.05s 
220069     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmodUnique2 
221060     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmodUnique2 
221178     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 105.89ms 
221181     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_intDivRem.proof 
221182     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 429ns 
221183     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
224230     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.05s 
224230     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: intDivRem 
225213     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: intDivRem 
225217     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.76ms 
225219     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmodjmod.proof 
225219     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 374.8ns 
225220     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
228209     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.99s 
228209     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmodjmod 
229205     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmodjmod 
229262     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 49.53ms 
229264     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmodDivisible.proof 
229264     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 97.7ns 
229265     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
232424     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.16s 
232424     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmodDivisible 
233378     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmodDivisible 
233411     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 28.34ms 
233414     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmodDivisibleRep.proof 
233414     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 305.2ns 
233416     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
236508     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.09s 
236508     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmodDivisibleRep 
237515     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmodDivisibleRep 
237522     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.18ms 
237527     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdivAddMultDenom.proof 
237527     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 79.1ns 
237529     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
240583     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.05s 
240583     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdivAddMultDenom 
241565     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdivAddMultDenom 
241765     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 186.71ms 
241768     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmodAltZero.proof 
241768     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 317.4ns 
241769     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
244832     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.06s 
244832     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmodAltZero 
245796     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmodAltZero 
245809     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 10.22ms 
245812     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmodAddMultDenomZero.proof 
245812     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 306.4ns 
245813     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
248796     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.98s 
248796     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmodAddMultDenomZero 
249803     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmodAddMultDenomZero 
249814     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 8.27ms 
249815     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_polyDiv_zero.proof 
249815     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 113.2ns 
249816     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
252889     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.07s 
252890     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: polyDiv_zero 
253866     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: polyDiv_zero 
253892     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 23.47ms 
253894     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_polyMod_ltdivDenom.proof 
253894     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 100.7ns 
253895     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
257005     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.11s 
257005     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: polyMod_ltdivDenom 
257975     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: polyMod_ltdivDenom 
257990     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 8.01ms 
257992     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_empty.proof 
257992     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 65.7ns 
257993     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
261003     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.01s 
261003     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_empty 
261998     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_empty 
262002     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.74ms 
262003     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_induction_upper.proof 
262003     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 82ns 
262004     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
265078     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.07s 
265078     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_upper 
266079     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_induction_upper 
266084     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.49ms 
266086     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_induction_lower.proof 
266086     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 74.1ns 
266087     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
269087     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3s 
269087     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_lower 
270102     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_induction_lower 
270133     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 26.44ms 
270135     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_bounds.proof 
270135     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 72.4ns 
270136     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
273207     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.07s 
273207     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_bounds 
274149     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_bounds 
274171     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 19.85ms 
274174     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_bounds2.proof 
274174     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 69.6ns 
274175     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
277231     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.06s 
277231     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_bounds2 
278232     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_bounds2 
278251     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 15.1ms 
278255     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_induction_upper2.proof 
278255     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 277.2ns 
278259     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
281362     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.1s 
281363     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_upper2 
282344     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_induction_upper2 
282348     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.53ms 
282349     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_induction_upper_concrete.proof 
282349     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 77.4ns 
282350     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
285327     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.98s 
285327     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_upper_concrete 
286297     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_induction_upper_concrete 
286302     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.06ms 
286304     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_induction_upper_concrete_2.proof 
286304     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 111.5ns 
286306     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
289290     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.98s 
289290     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_upper_concrete_2 
290282     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_induction_upper_concrete_2 
290288     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.27ms 
290290     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_induction_upper2_concrete.proof 
290290     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 78.6ns 
290291     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
293396     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.11s 
293396     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_upper2_concrete 
294348     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_induction_upper2_concrete 
294352     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.32ms 
294354     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_induction_lower_concrete.proof 
294354     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 77.4ns 
294355     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
297418     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.06s 
297419     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_lower_concrete 
298387     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_induction_lower_concrete 
298391     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 832.4ns 
298394     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_induction_lower2.proof 
298395     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 270.5ns 
298396     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
301461     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.06s 
301461     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_lower2 
302473     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_induction_lower2 
302477     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.41ms 
302478     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_induction_lower2_concrete.proof 
302478     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 75.8ns 
302479     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
305549     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.07s 
305549     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_lower2_concrete 
306535     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_induction_lower2_concrete 
306537     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.03ms 
306539     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_positive.proof 
306539     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 80.9ns 
306540     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
309648     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.11s 
309648     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_positive 
310651     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_positive 
310706     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 51.31ms 
310708     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_upper_bound.proof 
310709     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 245.9ns 
310710     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
313834     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.12s 
313834     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_upper_bound 
314812     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_upper_bound 
314855     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 38.86ms 
314857     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_lower_bound.proof 
314858     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 242.9ns 
314859     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
318035     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.18s 
318036     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_lower_bound 
319040     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_lower_bound 
319076     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 31.75ms 
319078     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_positive_lower_bound_element.proof 
319079     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 288.1ns 
319080     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
322153     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.07s 
322153     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_positive_lower_bound_element 
323166     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_positive_lower_bound_element 
323214     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 43.39ms 
323216     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_sub_same_index.proof 
323216     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 66.7ns 
323217     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
326258     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.04s 
326258     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_sub_same_index 
327274     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_sub_same_index 
327304     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 25.47ms 
327305     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_less_same_index.proof 
327305     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 101.9ns 
327306     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
330373     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.07s 
330373     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_less_same_index 
331359     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_less_same_index 
331431     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 66.17ms 
331433     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_equal_except_one_index.proof 
331433     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 179.9ns 
331434     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
334496     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.06s 
334497     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_equal_except_one_index 
335439     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_equal_except_one_index 
335467     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 23.81ms 
335468     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_is_max.proof 
335468     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 73.1ns 
335469     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
338543     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.07s 
338543     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_is_max 
339522     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_is_max 
339545     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 19.56ms 
339547     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_is_max2.proof 
339547     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 82.7ns 
339548     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
342597     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.05s 
342598     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_is_max2 
343573     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_is_max2 
343597     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 20.79ms 
343599     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_is_max3.proof 
343599     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 74.3ns 
343600     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
346642     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.04s 
346642     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_is_max3 
347621     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_is_max3 
347644     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 18.75ms 
347645     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_is_max4.proof 
347645     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 84.2ns 
347646     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
350731     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.08s 
350732     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_is_max4 
351722     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_is_max4 
351752     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 26.08ms 
351754     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_lt_max.proof 
351754     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 81.4ns 
351755     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
354839     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.08s 
354839     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_lt_max 
355831     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_lt_max 
355865     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 27.47ms 
355867     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_lt_max2.proof 
355867     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 94.1ns 
355868     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
358911     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.04s 
358911     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_lt_max2 
359917     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_lt_max2 
359951     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 30.08ms 
359953     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_lt_max3.proof 
359953     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 105.9ns 
359954     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
362998     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.04s 
362999     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_lt_max3 
363935     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_lt_max3 
363958     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 20.16ms 
363960     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_lt_max4.proof 
363960     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 77ns 
363961     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
366991     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.03s 
366991     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_lt_max4 
367962     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_lt_max4 
367986     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 20.94ms 
367988     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_gt0.proof 
367988     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 86.2ns 
367989     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
371036     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.05s 
371036     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_gt0 
372032     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_gt0 
372059     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 22.71ms 
372061     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_gt0_alt.proof 
372062     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 397ns 
372063     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
375116     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.05s 
375116     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_gt0_alt 
376114     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_gt0_alt 
376142     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 24.93ms 
376144     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_add_concrete.proof 
376144     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 87.5ns 
376145     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
379193     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.05s 
379193     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_add_concrete 
380172     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_add_concrete 
380179     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 5.16ms 
380181     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bprod/Taclet_bprod_all_positive.proof 
380181     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 72ns 
380182     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
383229     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.05s 
383230     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bprod_all_positive 
384189     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bprod_all_positive 
384207     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 14.53ms 
384208     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bprod/Taclet_bprod_split.proof 
384208     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 62.3ns 
384209     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
387236     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.03s 
387236     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bprod_split 
388219     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bprod_split 
388226     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.47ms 
388227     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powConcrete0.proof 
388227     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 75.2ns 
388228     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
391265     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.04s 
391266     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powConcrete0 
392264     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powConcrete0 
392267     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 802.9ns 
392269     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powConcrete1.proof 
392270     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 207.8ns 
392271     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
395304     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.03s 
395305     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powConcrete1 
396297     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powConcrete1 
396300     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.19ms 
396302     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powSplitFactor.proof 
396302     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 93.5ns 
396303     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
399328     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.02s 
399329     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powSplitFactor 
400323     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powSplitFactor 
400339     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 13.09ms 
400341     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powAdd.proof 
400341     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 102.4ns 
400343     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
403414     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.07s 
403414     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powAdd 
404364     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powAdd 
404371     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.84ms 
404373     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powMono.proof 
404373     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 94.6ns 
404374     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
407440     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.07s 
407440     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powMono 
408434     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powMono 
408452     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 14.78ms 
408454     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powMonoConcrete.proof 
408454     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 97.2ns 
408455     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
411529     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.07s 
411529     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powMonoConcrete 
412549     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powMonoConcrete 
412554     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.39ms 
412555     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powMonoConcreteRight.proof 
412555     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 62.9ns 
412556     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
415601     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.04s 
415601     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powMonoConcreteRight 
416577     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powMonoConcreteRight 
416579     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 683.21ns 
416581     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powPositive.proof 
416581     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 75.3ns 
416582     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
419616     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.03s 
419616     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powPositive 
420577     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powPositive 
420583     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.07ms 
420585     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powPositiveConcrete.proof 
420585     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 82.9ns 
420586     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
423702     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.12s 
423703     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powPositiveConcrete 
424658     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powPositiveConcrete 
424660     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 804.51ns 
424662     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powGeq1Concrete.proof 
424662     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 60.1ns 
424663     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
427754     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.09s 
427754     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powGeq1Concrete 
428722     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powGeq1Concrete 
428727     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.37ms 
428729     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_pow2InIntLower.proof 
428729     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 85.7ns 
428730     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
431743     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.01s 
431743     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: pow2InIntLower 
432753     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: pow2InIntLower 
432756     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 818.51ns 
432757     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_pow2InIntUpper.proof 
432758     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 85.8ns 
432758     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
435790     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.03s 
435790     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: pow2InIntUpper 
436769     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: pow2InIntUpper 
436774     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.96ms 
436775     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logSelfConcrete.proof 
436776     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 66.3ns 
436776     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
439811     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.03s 
439811     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logSelfConcrete 
440769     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logSelfConcrete 
440779     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 6.9ms 
440781     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_log1Concrete.proof 
440781     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 86.9ns 
440782     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
443815     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.03s 
443815     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: log1Concrete 
444757     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: log1Concrete 
444761     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.24ms 
444762     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logProduct.proof 
444762     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 74.2ns 
444763     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
447810     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.05s 
447810     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logProduct 
448770     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logProduct 
448778     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 5.65ms 
448780     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logTimesBaseConcrete.proof 
448780     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 228.9ns 
448781     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
451797     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.02s 
451797     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logTimesBaseConcrete 
452805     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logTimesBaseConcrete 
452810     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.23ms 
452812     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logProdIdentity.proof 
452812     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 129.2ns 
452813     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
455828     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.02s 
455828     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logProdIdentity 
456813     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logProdIdentity 
456840     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 23.5ms 
456842     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logProdIdentityConcrete.proof 
456842     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 94.1ns 
456843     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
459854     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.01s 
459854     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logProdIdentityConcrete 
460829     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logProdIdentityConcrete 
460833     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.53ms 
460835     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logPowIdentity.proof 
460835     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 74.8ns 
460836     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
463898     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.06s 
463898     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logPowIdentity 
464883     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logPowIdentity 
464887     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.67ms 
464889     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logPowIdentityConcrete.proof 
464889     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 70.8ns 
464890     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
467949     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.06s 
467949     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logPowIdentityConcrete 
468920     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logPowIdentityConcrete 
468925     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.53ms 
468926     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logPositive.proof 
468926     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 76.5ns 
468927     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
471981     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.05s 
471981     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logPositive 
472995     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logPositive 
473015     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 15.45ms 
473016     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logPositiveConcrete.proof 
473016     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 73.2ns 
473017     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
476089     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.07s 
476089     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logPositiveConcrete 
477076     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logPositiveConcrete 
477082     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 617.11ns 
477084     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logMono.proof 
477086     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 1.78ms 
477087     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
480119     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.03s 
480119     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logMono 
481089     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logMono 
481134     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 40.39ms 
481136     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logMonoConcrete.proof 
481136     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 84.3ns 
481137     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
484187     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.05s 
484187     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logMonoConcrete 
485189     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logMonoConcrete 
485194     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.72ms 
485198     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powLogLess.proof 
485198     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 87.2ns 
485199     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
488226     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.03s 
488226     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powLogLess 
489196     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powLogLess 
489219     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 19.02ms 
489220     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powLogMore2.proof 
489221     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 83.5ns 
489221     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
492268     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.05s 
492268     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powLogMore2 
493263     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powLogMore2 
493284     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 17.84ms 
493286     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logLessThanPow.proof 
493286     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 79.2ns 
493287     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
496291     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3s 
496291     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logLessThanPow 
497246     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logLessThanPow 
497272     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 22.34ms 
497274     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logLessThanPowConcrete.proof 
497274     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 79.4ns 
497275     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
500349     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.07s 
500349     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logLessThanPowConcrete 
501301     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logLessThanPowConcrete 
501304     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 624.61ns 
501305     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logSqueeze.proof 
501305     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 56.9ns 
501306     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
504394     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.09s 
504394     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logSqueeze 
505370     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logSqueeze 
505377     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.49ms 
505378     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/booleanRules/Taclet_ifthenelse_equals.proof 
505378     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 60.3ns 
505379     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
508371     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.99s 
508371     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: ifthenelse_equals 
509339     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: ifthenelse_equals 
509343     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.08ms 
509345     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/booleanRules/Taclet_ifthenelse_equals_1.proof 
509345     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 76.7ns 
509346     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
512359     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.01s 
512359     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: ifthenelse_equals_1 
513358     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: ifthenelse_equals_1 
513361     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.28ms 
513363     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/booleanRules/Taclet_ifthenelse_equals_2.proof 
513363     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 66.3ns 
513364     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
516374     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.01s 
516374     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: ifthenelse_equals_2 
517345     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: ifthenelse_equals_2 
517348     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.06ms 
517350     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/locSet/Taclet_disjointWithSingleton1.proof 
517350     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 82ns 
517350     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
520411     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.06s 
520412     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: disjointWithSingleton1 
521401     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: disjointWithSingleton1 
521405     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.78ms 
521407     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/locSet/Taclet_disjointWithSingleton2.proof 
521407     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 57.6ns 
521408     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
524494     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.09s 
524494     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: disjointWithSingleton2 
525508     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: disjointWithSingleton2 
525511     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.7ms 
525513     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/locSet/Taclet_disjointArrayRanges.proof 
525513     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 61.9ns 
525514     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
528620     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.11s 
528621     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: disjointArrayRanges 
529643     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: disjointArrayRanges 
529655     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 8.54ms 
529656     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/locSet/Taclet_disjointArrayRangeAllFields1.proof 
529656     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 65ns 
529657     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
532876     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.22s 
532877     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: disjointArrayRangeAllFields1 
533914     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: disjointArrayRangeAllFields1 
533925     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 8.44ms 
533927     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/locSet/Taclet_disjointArrayRangeAllFields2.proof 
533927     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 68.1ns 
533928     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
537114     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.19s 
537114     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: disjointArrayRangeAllFields2 
538183     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: disjointArrayRangeAllFields2 
538193     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 7.02ms 
538195     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqSelfDefinition.proof 
538195     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 66.3ns 
538195     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
541396     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.2s 
541396     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqSelfDefinition 
542444     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqSelfDefinition 
542454     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 7.4ms 
542456     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqOutsideValue.proof 
542456     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 112.2ns 
542457     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
545507     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.05s 
545507     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqOutsideValue 
546497     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqOutsideValue 
546501     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.84ms 
546503     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_castedGetAny.proof 
546503     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 76.4ns 
546504     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
549544     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.04s 
549545     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: castedGetAny 
550535     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: castedGetAny 
550540     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.33ms 
550542     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqGetAlphaCast.proof 
550542     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 71.5ns 
550543     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
553673     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.13s 
553674     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqGetAlphaCast 
554677     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqGetAlphaCast 
554680     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 952.51ns 
554681     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqSingleton.proof 
554681     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 77.6ns 
554682     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
557686     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3s 
557687     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqSingleton 
558686     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqSingleton 
558689     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.11ms 
558690     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqSingletonConcrete.proof 
558690     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 75.9ns 
558691     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
561750     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.06s 
561750     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqSingletonConcrete 
562746     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqSingletonConcrete 
562749     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.1ms 
562750     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqConcat.proof 
562750     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 83.6ns 
562751     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
565765     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.01s 
565765     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqConcat 
566749     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqConcat 
566762     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 10.52ms 
566763     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqSub.proof 
566763     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 76.2ns 
566764     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
569789     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.02s 
569789     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqSub 
570777     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqSub 
570781     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.7ms 
570782     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqReverse.proof 
570782     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 72.1ns 
570783     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
573873     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.09s 
573873     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqReverse 
574869     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqReverse 
574877     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 6.09ms 
574879     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqEmpty.proof 
574879     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 73.8ns 
574880     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
577893     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.01s 
577893     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqEmpty 
578873     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqEmpty 
578876     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 964.81ns 
578878     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqSingleton.proof 
578878     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 84.9ns 
578879     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
581919     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.04s 
581919     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqSingleton 
582892     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqSingleton 
582894     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 772.51ns 
582896     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqConcat.proof 
582896     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 73.1ns 
582897     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
585924     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.03s 
585924     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqConcat 
586912     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqConcat 
586916     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.15ms 
586917     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqSub.proof 
586917     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 136.4ns 
586918     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
589912     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.99s 
589912     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqSub 
590904     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqSub 
590907     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.02ms 
590909     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqReverse.proof 
590909     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 59.8ns 
590910     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
594028     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.12s 
594028     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqReverse 
595011     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqReverse 
595015     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.42ms 
595016     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_equalityToSeqGetAndSeqLenLeft.proof 
595016     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 86.8ns 
595017     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
597997     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.98s 
597998     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: equalityToSeqGetAndSeqLenLeft 
598984     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: equalityToSeqGetAndSeqLenLeft 
598987     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.15ms 
598988     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_equalityToSeqGetAndSeqLenRight.proof 
598988     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 70.9ns 
598989     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
601996     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.01s 
601997     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: equalityToSeqGetAndSeqLenRight 
602995     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: equalityToSeqGetAndSeqLenRight 
603001     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.47ms 
603002     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqSingletonEQ.proof 
603003     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 121.1ns 
603003     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
605999     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3s 
605999     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqSingletonEQ 
607034     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqSingletonEQ 
607037     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.79ms 
607039     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqConcatEQ.proof 
607040     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 288.2ns 
607041     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
610205     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.16s 
610205     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqConcatEQ 
611242     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqConcatEQ 
611255     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 9.86ms 
611256     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqSubEQ.proof 
611256     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 210.7ns 
611257     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
614412     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.15s 
614412     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqSubEQ 
615398     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqSubEQ 
615400     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 671.71ns 
615402     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqReverseEQ.proof 
615402     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 61.5ns 
615404     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
618426     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.02s 
618426     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqReverseEQ 
619423     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqReverseEQ 
619431     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 5.86ms 
619433     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqEmptyEQ.proof 
619433     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 72.6ns 
619434     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
622505     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.07s 
622505     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqEmptyEQ 
623527     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqEmptyEQ 
623530     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.04ms 
623532     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqSingletonEQ.proof 
623532     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 76.6ns 
623533     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
626624     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.09s 
626624     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqSingletonEQ 
627642     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqSingletonEQ 
627645     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 935.91ns 
627647     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqConcatEQ.proof 
627648     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 81.7ns 
627648     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
630731     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.08s 
630731     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqConcatEQ 
631736     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqConcatEQ 
631740     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.5ms 
631742     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqSubEQ.proof 
631742     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 57.9ns 
631743     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
634852     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.11s 
634852     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqSubEQ 
635858     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqSubEQ 
635861     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.1ms 
635862     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqReverseEQ.proof 
635862     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 77.4ns 
635863     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
638927     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.06s 
638927     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqReverseEQ 
639953     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqReverseEQ 
639957     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.82ms 
639958     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqDefEQ.proof 
639958     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 73.8ns 
639959     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
643017     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.06s 
643017     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqDefEQ 
644027     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqDefEQ 
644031     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.59ms 
644033     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqDefEQ.proof 
644033     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 60.5ns 
644033     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
647091     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.06s 
647091     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqDefEQ 
648115     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqDefEQ 
648120     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.09ms 
648121     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqConcatWithSeqEmpty1.proof 
648121     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 61.1ns 
648122     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
651176     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.05s 
651176     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqConcatWithSeqEmpty1 
652192     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqConcatWithSeqEmpty1 
652203     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 8.04ms 
652204     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqConcatWithSeqEmpty2.proof 
652204     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 86.2ns 
652205     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
655224     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.02s 
655224     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqConcatWithSeqEmpty2 
656206     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqConcatWithSeqEmpty2 
656216     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 8.12ms 
656219     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqReverseOfSeqEmpty.proof 
656219     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 72.3ns 
656220     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
659294     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.07s 
659294     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqReverseOfSeqEmpty 
660288     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqReverseOfSeqEmpty 
660296     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 6.09ms 
660297     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_subSeqComplete.proof 
660297     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 75.2ns 
660298     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
663332     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.03s 
663332     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: subSeqComplete 
664321     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: subSeqComplete 
664331     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 7.25ms 
664332     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_subSeqTailR.proof 
664333     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 82.1ns 
664333     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
667327     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.99s 
667327     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: subSeqTailR 
668304     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: subSeqTailR 
668319     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 11.93ms 
668321     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_subSeqTailL.proof 
668321     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 70.5ns 
668322     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
671323     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3s 
671323     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: subSeqTailL 
672299     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: subSeqTailL 
672316     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 14.2ms 
672318     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_subSeqTailEQR.proof 
672318     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 82.2ns 
672319     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
675340     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.02s 
675340     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: subSeqTailEQR 
676292     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: subSeqTailEQR 
676308     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 12.85ms 
676310     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_subSeqTailEQL.proof 
676310     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 60.2ns 
676311     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
679274     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.96s 
679274     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: subSeqTailEQL 
680268     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: subSeqTailEQL 
680278     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 7.41ms 
680280     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDef_split.proof 
680280     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 89.8ns 
680281     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
683280     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3s 
683280     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_split 
684281     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDef_split 
684315     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 30.43ms 
684317     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDef_induction_upper.proof 
684317     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 67.6ns 
684318     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
687292     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.97s 
687292     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_induction_upper 
688256     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDef_induction_upper 
688301     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 28.75ms 
688303     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDef_induction_upper_concrete.proof 
688303     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 75.6ns 
688304     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
691274     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.97s 
691275     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_induction_upper_concrete 
692284     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDef_induction_upper_concrete 
692322     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 33.63ms 
692323     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDef_induction_lower.proof 
692323     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 77.3ns 
692324     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
695424     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.1s 
695425     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_induction_lower 
696422     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDef_induction_lower 
696449     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 23.76ms 
696451     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDef_induction_lower_concrete.proof 
696451     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 79.8ns 
696452     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
699476     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.02s 
699477     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_induction_lower_concrete 
700492     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDef_induction_lower_concrete 
700519     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 22.94ms 
700520     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDef_split_in_three.proof 
700520     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 62.5ns 
700521     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
703588     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.07s 
703588     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_split_in_three 
704593     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDef_split_in_three 
704696     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 96.16ms 
704698     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDef_empty.proof 
704698     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 63.7ns 
704699     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
707781     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.08s 
707782     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_empty 
708817     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDef_empty 
708823     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.87ms 
708825     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDef_one_summand.proof 
708825     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 91.4ns 
708826     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
711909     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.08s 
711909     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_one_summand 
712905     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDef_one_summand 
712912     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.27ms 
712913     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDef_lower_equals_upper.proof 
712913     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 82.5ns 
712914     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
715996     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.08s 
715996     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_lower_equals_upper 
716992     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDef_lower_equals_upper 
716997     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.67ms 
716998     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDefOfSeq.proof 
716998     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 72.1ns 
716999     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
720064     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.06s 
720064     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDefOfSeq 
721054     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDefOfSeq 
721072     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 14.46ms 
721074     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqSelfDefinitionEQ2.proof 
721074     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 79.5ns 
721075     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
724156     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.08s 
724156     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqSelfDefinitionEQ2 
725177     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqSelfDefinitionEQ2 
725185     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 5.77ms 
725186     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_indexOfSeqSingleton.proof 
725186     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 57.6ns 
725187     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
728234     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.05s 
728234     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: indexOfSeqSingleton 
729228     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: indexOfSeqSingleton 
729232     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.31ms 
729234     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_indexOfSeqConcatFirst.proof 
729234     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 73.8ns 
729235     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
732339     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.1s 
732339     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: indexOfSeqConcatFirst 
733372     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: indexOfSeqConcatFirst 
733387     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 12.84ms 
733390     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_indexOfSeqConcatSecond.proof 
733390     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 86.5ns 
733391     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
736438     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.05s 
736439     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: indexOfSeqConcatSecond 
737391     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: indexOfSeqConcatSecond 
737405     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 11.56ms 
737407     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_indexOfSeqSub.proof 
737407     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 69.2ns 
737407     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
740434     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.03s 
740434     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: indexOfSeqSub 
741407     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: indexOfSeqSub 
741428     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 17.7ms 
741459     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfArray2seq.proof 
741459     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 129.5ns 
741460     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
744559     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.1s 
744559     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfArray2seq 
745546     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfArray2seq 
745550     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.05ms 
745551     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getAnyOfArray2seq.proof 
745551     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 53.3ns 
745552     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
748524     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.97s 
748524     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getAnyOfArray2seq 
749529     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getAnyOfArray2seq 
749533     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.05ms 
749535     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfArray2seq.proof 
749535     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 95ns 
749536     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
752625     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.09s 
752625     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfArray2seq 
753635     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfArray2seq 
753642     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 5.46ms 
753644     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_getAnyOfNPermInv.proof 
753644     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 110.2ns 
753644     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
756674     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.03s 
756675     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getAnyOfNPermInv 
757643     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getAnyOfNPermInv 
757649     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.84ms 
757650     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqNPermRange.proof 
757650     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 67.1ns 
757651     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
760654     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3s 
760654     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqNPermRange 
761663     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqNPermRange 
761723     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 52.43ms 
761724     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermTrans.proof 
761725     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 76.6ns 
761725     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
764817     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.09s 
764817     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermTrans 
765826     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermTrans 
765851     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 20.96ms 
765853     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermRefl.proof 
765853     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 139.3ns 
765854     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
768945     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.09s 
768946     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermRefl 
769963     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermRefl 
769979     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 12.44ms 
769980     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermSplit.proof 
769980     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 62.2ns 
769981     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
773031     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.05s 
773032     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermSplit 
774030     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermSplit 
774033     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 241.4ns 
774034     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqNPermRight.proof 
774034     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 57ns 
774035     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
777077     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.04s 
777077     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqNPermRight 
778050     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqNPermRight 
778169     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 105.92ms 
778171     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermFromSwap.proof 
778171     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 212.2ns 
778172     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
781195     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.02s 
781195     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermFromSwap 
782180     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermFromSwap 
782264     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 78.09ms 
782266     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermTransAlt0.proof 
782266     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 59.9ns 
782266     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
785273     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.01s 
785273     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermTransAlt0 
786289     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermTransAlt0 
786291     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 240.7ns 
786293     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermTransAlt1.proof 
786293     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 61.5ns 
786294     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
789343     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.05s 
789343     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermTransAlt1 
790315     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermTransAlt1 
790317     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 328.2ns 
790319     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermTransAlt2.proof 
790319     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 78.7ns 
790320     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
793291     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.97s 
793291     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermTransAlt2 
794306     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermTransAlt2 
794309     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 287.1ns 
794310     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermTransAlt3.proof 
794310     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 79.3ns 
794311     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
797352     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.04s 
797353     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermTransAlt3 
798360     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermTransAlt3 
798363     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 607.11ns 
798364     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermForall.proof 
798364     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 74.9ns 
798365     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
801416     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.05s 
801416     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermForall 
802442     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermForall 
802560     INFO  Test worker     d.u.i.k.s.SMTFocusResults Analyzing unsat core: (L_1 L_3 L_4) 
802576     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 131.43ms 
802578     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermExists.proof 
802578     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 111.3ns 
802579     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
805748     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.17s 
805748     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermExists 
806797     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermExists 
806848     INFO  Test worker     d.u.i.k.s.SMTFocusResults Analyzing unsat core: (L_1 L_3 L_5 L_6 L_7) 
806849     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 48.96ms 
806850     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm2/Taclet_schiffl_lemma_2.proof 
806850     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 83.2ns 
806851     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
810120     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.27s 
810120     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: schiffl_lemma_2 
811264     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: schiffl_lemma_2 
811266     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.1ns 
811316     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [1] goal: 0, source line: 49, command: 'macro split-prop' 
811394     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [2] goal: 3, source line: 50, command: 'rule allRight' 
811437     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [3] goal: 4, source line: 51, command: 'rule allRight' 
811443     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [4] goal: 5, source line: 52, command: 'macro split-prop' 
811479     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [5] goal: 11, source line: 53, command: 'rule 'seqPermDefLeft'' 
811481     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [6] goal: 12, source line: 54, command: 'rule 'andLeft'' 
811484     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [7] goal: 13, source line: 55, command: 'rule 'exLeft'' 
811488     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [8] goal: 14, source line: 56, command: 'macro split-prop' 
811494     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [9] goal: 16, source line: 57, command: 'rule  seqNPermRange' 
811497     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [10] goal: 17, source line: 59, command: 'instantiate var=iv with='v_x_0' occ=1' 
811499     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [11] goal: 18, source line: 60, command: 'rule impLeft' 
811502     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [12] goal: 19, source line: 61, command: 'tryclose branch' 
811867     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [13] goal: 20, source line: 62, command: 'rule andLeft' 
811868     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [14] goal: 97, source line: 63, command: 'rule andLeft' 
811870     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [15] goal: 98, source line: 64, command: 'instantiate var=iv with='v_y_0' occ=1' 
811871     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [16] goal: 99, source line: 66, command: 'rule impLeft' 
811872     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [17] goal: 100, source line: 67, command: 'tryclose branch' 
812046     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [18] goal: 101, source line: 68, command: 'rule andLeft' 
812047     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [19] goal: 188, source line: 69, command: 'rule andLeft' 
812048     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [20] goal: 189, source line: 70, command: 'rule seqNPermDefLeft' 
812050     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [21] goal: 190, source line: 72, command: 'instantiate var=iv with='v_x_0' occ=2' 
812052     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [22] goal: 191, source line: 73, command: 'rule impLeft' 
812054     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [23] goal: 192, source line: 74, command: 'tryclose branch' 
812284     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [24] goal: 193, source line: 75, command: 'rule exLeft' 
812286     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [25] goal: 310, source line: 76, command: 'rule andLeft' 
812287     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [26] goal: 311, source line: 77, command: 'rule andLeft' 
812288     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [27] goal: 312, source line: 78, command: 'instantiate hide var=iv with='v_y_0' occ=2' 
812289     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [28] goal: 313, source line: 80, command: 'rule impLeft' 
812291     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [29] goal: 314, source line: 81, command: 'tryclose branch' 
812464     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [30] goal: 315, source line: 82, command: 'rule exLeft' 
812466     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [31] goal: 420, source line: 83, command: 'rule andLeft' 
812468     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [32] goal: 421, source line: 84, command: 'rule andLeft' 
812469     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [33] goal: 422, source line: 85, command: 'instantiate var=iv with='jv_0' occ=1' 
812470     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [34] goal: 423, source line: 87, command: 'rule impLeft' 
812471     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [35] goal: 424, source line: 88, command: 'tryclose branch' 
812482     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [36] goal: 425, source line: 89, command: 'rule andLeft' 
812483     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [37] goal: 434, source line: 90, command: 'rule andLeft' 
812485     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [38] goal: 435, source line: 91, command: 'rule castAdd formula='s_0[jv_0] = v_x_0' occ=0' 
812486     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [39] goal: 436, source line: 92, command: 'instantiate hide var=iv with='jv_1' occ=1' 
812487     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [40] goal: 437, source line: 94, command: 'rule impLeft' 
812488     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [41] goal: 438, source line: 95, command: 'tryclose branch' 
812498     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [42] goal: 439, source line: 96, command: 'rule andLeft' 
812499     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [43] goal: 448, source line: 97, command: 'rule andLeft' 
812500     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [44] goal: 449, source line: 98, command: 'rule castAdd formula='s_0[jv_1] = v_y_0' occ=0' 
812501     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [45] goal: 450, source line: 99, command: 'instantiate var=iv  with='v_x_0'' 
812502     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [46] goal: 451, source line: 101, command: 'rule impLeft' 
812503     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [47] goal: 452, source line: 102, command: 'tryclose branch' 
812709     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [48] goal: 453, source line: 103, command: 'instantiate var=iv  with='v_y_0'' 
812710     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [49] goal: 562, source line: 105, command: 'rule impLeft' 
812712     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [50] goal: 563, source line: 106, command: 'tryclose branch' 
812883     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [51] goal: 564, source line: 107, command: 'cut 'v_x_0 = v_y_0'' 
812884     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [52] goal: 674, source line: 109, command: 'instantiate hide var='v_r' with='seqSwap(s_0,v_x_0,jv_0)'' 
812886     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [53] goal: 676, source line: 111, command: 'rule andRight' 
812888     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [54] goal: 677, source line: 113, command: 'rule andRight' 
812889     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [55] goal: 679, source line: 114, command: 'rule andRight' 
812890     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [56] goal: 681, source line: 115, command: 'rule andRight' 
812891     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [57] goal: 683, source line: 116, command: 'rule lenOfSwap' 
812892     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [58] goal: 685, source line: 117, command: 'tryclose branch' 
812898     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [59] goal: 684, source line: 118, command: 'rule seqNPermSwapNPerm' 
812899     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [60] goal: 687, source line: 120, command: 'instantiate hide var='iv' with='v_x_0' occ=1' 
812900     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [61] goal: 688, source line: 121, command: 'instantiate hide var='jv' with='jv_0'' 
812903     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [62] goal: 689, source line: 122, command: 'rule impLeft' 
812904     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [63] goal: 690, source line: 123, command: 'tryclose branch' 
813050     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [64] goal: 691, source line: 124, command: 'tryclose branch' 
813055     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [65] goal: 682, source line: 125, command: 'rule allRight' 
813056     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [66] goal: 796, source line: 127, command: 'rule impRight' 
813058     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [67] goal: 797, source line: 128, command: 'rule andLeft' 
813059     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [68] goal: 798, source line: 129, command: 'instantiate var=iv with='v_iv_0'' 
813059     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [69] goal: 799, source line: 130, command: 'rule impLeft' 
813061     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [70] goal: 800, source line: 131, command: 'tryclose branch' 
813213     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [71] goal: 801, source line: 132, command: 'rule getOfSwap' 
813215     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [72] goal: 912, source line: 133, command: 'rule ifthenelse_negated' 
813216     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [73] goal: 913, source line: 134, command: 'rule ifthenelse_split occ=0' 
813218     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [74] goal: 914, source line: 135, command: 'rule andLeft' 
813219     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [75] goal: 916, source line: 136, command: 'rule andLeft' 
813222     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [76] goal: 917, source line: 137, command: 'rule andLeft' 
813223     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [77] goal: 918, source line: 138, command: 'rule ifthenelse_split occ=0' 
813224     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [78] goal: 919, source line: 139, command: 'tryclose branch' 
813354     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [79] goal: 920, source line: 140, command: 'rule ifthenelse_split occ=0' 
813356     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [80] goal: 1011, source line: 141, command: 'tryclose branch' 
813552     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [81] goal: 1012, source line: 142, command: 'tryclose branch' 
813561     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [82] goal: 915, source line: 143, command: 'tryclose branch' 
813572     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [83] goal: 680, source line: 144, command: 'rule getOfSwap' 
813573     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [84] goal: 1099, source line: 146, command: 'rule ifthenelse_negated' 
813575     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [85] goal: 1100, source line: 147, command: 'rule ifthenelse_split occ=0' 
813576     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [86] goal: 1101, source line: 148, command: 'rule andLeft' 
813577     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [87] goal: 1103, source line: 149, command: 'rule andLeft' 
813578     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [88] goal: 1104, source line: 150, command: 'rule andLeft' 
813579     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [89] goal: 1105, source line: 151, command: 'rule ifthenelse_split occ=0' 
813580     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [90] goal: 1106, source line: 152, command: 'tryclose branch' 
813590     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [91] goal: 1107, source line: 153, command: 'tryclose branch' 
813596     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [92] goal: 1102, source line: 154, command: 'tryclose branch' 
813717     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [93] goal: 678, source line: 155, command: 'rule getOfSwap' 
813718     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [94] goal: 1225, source line: 157, command: 'rule ifthenelse_negated' 
813719     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [95] goal: 1226, source line: 158, command: 'rule ifthenelse_split occ=0' 
813721     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [96] goal: 1227, source line: 159, command: 'rule andLeft' 
813722     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [97] goal: 1229, source line: 160, command: 'rule andLeft' 
813722     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [98] goal: 1230, source line: 161, command: 'rule andLeft' 
813723     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [99] goal: 1231, source line: 162, command: 'rule ifthenelse_split occ=0' 
813724     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [100] goal: 1232, source line: 163, command: 'tryclose branch' 
813840     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [101] goal: 1233, source line: 164, command: 'tryclose branch' 
813848     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [102] goal: 1228, source line: 165, command: 'tryclose branch' 
813965     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [103] goal: 675, source line: 166, command: 'cut '(int)s_0[v_x_0] = (int)s_0[v_y_0]'' 
813966     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [104] goal: 1397, source line: 169, command: 'rule seqNPermInjective' 
813967     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [105] goal: 1399, source line: 170, command: 'instantiate hide var=iv with='v_x_0'' 
813969     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [106] goal: 1400, source line: 171, command: 'instantiate hide var=jv with='v_y_0'' 
813970     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [107] goal: 1401, source line: 172, command: 'rule impLeft' 
813972     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [108] goal: 1402, source line: 173, command: 'tryclose branch' 
814174     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [109] goal: 1403, source line: 174, command: 'tryclose branch' 
814180     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [110] goal: 1398, source line: 175, command: 'cut '(int)s_0[v_x_0] = v_x_0'' 
814183     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [111] goal: 1534, source line: 177, command: 'instantiate hide var=v_r with='seqSwap(s_0,v_y_0,jv_1)'' 
814185     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [112] goal: 1536, source line: 179, command: 'rule andRight' 
814187     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [113] goal: 1537, source line: 181, command: 'rule andRight' 
814190     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [114] goal: 1539, source line: 182, command: 'rule andRight' 
814191     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [115] goal: 1541, source line: 183, command: 'rule andRight' 
814192     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [116] goal: 1543, source line: 184, command: 'tryclose branch' 
814207     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [117] goal: 1544, source line: 185, command: 'rule seqNPermSwapNPerm' 
814216     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [118] goal: 1558, source line: 187, command: 'instantiate hide var=iv with='v_y_0'' 
814218     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [119] goal: 1559, source line: 188, command: 'instantiate hide var=jv with='jv_1'' 
814219     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [120] goal: 1560, source line: 189, command: 'tryclose branch' 
814360     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [121] goal: 1542, source line: 190, command: 'rule allRight' 
814362     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [122] goal: 1667, source line: 192, command: 'rule impRight' 
814370     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [123] goal: 1668, source line: 193, command: 'rule andLeft' 
814372     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [124] goal: 1669, source line: 194, command: 'instantiate var=iv with='v_iv_0'' 
814372     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [125] goal: 1670, source line: 195, command: 'rule impLeft' 
814374     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [126] goal: 1671, source line: 196, command: 'tryclose branch' 
814519     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [127] goal: 1672, source line: 197, command: 'rule getOfSwap' 
814520     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [128] goal: 1786, source line: 198, command: 'rule ifthenelse_negated' 
814522     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [129] goal: 1787, source line: 199, command: 'rule ifthenelse_split occ=0' 
814525     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [130] goal: 1788, source line: 200, command: 'rule andLeft' 
814526     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [131] goal: 1790, source line: 201, command: 'rule andLeft' 
814527     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [132] goal: 1791, source line: 202, command: 'rule andLeft' 
814528     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [133] goal: 1792, source line: 203, command: 'rule ifthenelse_split occ=0' 
814529     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [134] goal: 1793, source line: 204, command: 'tryclose branch' 
814635     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [135] goal: 1794, source line: 205, command: 'rule ifthenelse_split occ=0' 
814638     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [136] goal: 1885, source line: 206, command: 'tryclose branch' 
814733     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [137] goal: 1886, source line: 207, command: 'instantiate var=iv with='v_y_0'' 
814734     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [138] goal: 1968, source line: 208, command: 'rule impLeft' 
814735     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [139] goal: 1969, source line: 209, command: 'tryclose branch' 
814741     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [140] goal: 1970, source line: 210, command: 'tryclose branch' 
814745     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [141] goal: 1789, source line: 211, command: 'tryclose branch' 
814751     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [142] goal: 1540, source line: 212, command: 'tryclose branch' 
814937     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [143] goal: 1538, source line: 213, command: 'rule getOfSwap' 
814940     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [144] goal: 2097, source line: 215, command: 'rule ifthenelse_negated' 
814941     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [145] goal: 2098, source line: 216, command: 'rule ifthenelse_split occ=0' 
814942     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [146] goal: 2099, source line: 217, command: 'tryclose branch' 
814956     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [147] goal: 2100, source line: 218, command: 'tryclose branch' 
815080     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [148] goal: 1535, source line: 219, command: 'tryclose branch' 
819665     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [149] goal: 1535, source line: 221, command: 'cut  '(int)s_0[v_y_0] = v_y_0'' 
819666     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [150] goal: 4266, source line: 224, command: 'instantiate hide var=v_r with='seqSwap(s_0,v_x_0,jv_0)'' 
819671     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [151] goal: 4268, source line: 226, command: 'rule andRight' 
819673     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [152] goal: 4269, source line: 228, command: 'rule andRight' 
819674     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [153] goal: 4271, source line: 229, command: 'rule andRight' 
819675     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [154] goal: 4273, source line: 230, command: 'rule andRight' 
819676     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [155] goal: 4275, source line: 231, command: 'tryclose branch' 
819688     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [156] goal: 4276, source line: 232, command: 'rule seqNPermSwapNPerm' 
819689     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [157] goal: 4287, source line: 234, command: 'instantiate hide var=iv with='v_x_0'' 
819690     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [158] goal: 4288, source line: 235, command: 'instantiate hide var=jv with='jv_0'' 
819691     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [159] goal: 4289, source line: 236, command: 'rule impLeft' 
819693     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [160] goal: 4290, source line: 237, command: 'tryclose branch' 
819816     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [161] goal: 4291, source line: 238, command: 'tryclose branch' 
819821     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [162] goal: 4274, source line: 239, command: 'rule allRight' 
819822     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [163] goal: 4400, source line: 241, command: 'rule impRight' 
819823     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [164] goal: 4401, source line: 242, command: 'rule andLeft' 
819824     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [165] goal: 4402, source line: 243, command: 'instantiate var=iv with='v_iv_0'' 
819825     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [166] goal: 4403, source line: 244, command: 'rule impLeft' 
819826     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [167] goal: 4404, source line: 245, command: 'tryclose branch' 
819941     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [168] goal: 4405, source line: 246, command: 'rule getOfSwap' 
819943     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [169] goal: 4521, source line: 247, command: 'rule ifthenelse_negated' 
819944     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [170] goal: 4522, source line: 248, command: 'rule ifthenelse_split occ=0' 
819945     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [171] goal: 4523, source line: 249, command: 'rule andLeft' 
819946     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [172] goal: 4525, source line: 250, command: 'rule andLeft' 
819947     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [173] goal: 4526, source line: 251, command: 'rule andLeft' 
819948     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [174] goal: 4527, source line: 252, command: 'rule ifthenelse_split occ=0' 
819949     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [175] goal: 4528, source line: 253, command: 'tryclose branch' 
820043     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [176] goal: 4529, source line: 254, command: 'rule ifthenelse_split occ=0' 
820045     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [177] goal: 4622, source line: 255, command: 'tryclose branch' 
820141     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [178] goal: 4623, source line: 256, command: 'tryclose branch' 
820147     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [179] goal: 4524, source line: 257, command: 'tryclose branch' 
820153     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [180] goal: 4272, source line: 258, command: 'rule getOfSwap' 
820154     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [181] goal: 4713, source line: 260, command: 'rule ifthenelse_negated' 
820155     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [182] goal: 4714, source line: 261, command: 'rule ifthenelse_split occ=0' 
820156     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [183] goal: 4715, source line: 262, command: 'tryclose branch' 
820170     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [184] goal: 4716, source line: 263, command: 'tryclose branch' 
820276     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [185] goal: 4270, source line: 264, command: 'rule getOfSwap' 
820277     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [186] goal: 4839, source line: 266, command: 'rule ifthenelse_negated' 
820278     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [187] goal: 4840, source line: 267, command: 'rule ifthenelse_split occ=0' 
820279     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [188] goal: 4841, source line: 268, command: 'tryclose branch' 
820372     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [189] goal: 4842, source line: 269, command: 'tryclose branch' 
820385     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [190] goal: 4267, source line: 270, command: 'cut '(int)s_0[v_x_0]=v_y_0'' 
820386     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [191] goal: 4948, source line: 273, command: 'instantiate hide var=v_r with='seqSwap(seqSwap(s_0,jv_0,v_x_0),jv_0,v_y_0)'' 
820387     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [192] goal: 4950, source line: 275, command: 'rule andRight' 
820388     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [193] goal: 4951, source line: 277, command: 'rule andRight' 
820389     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [194] goal: 4953, source line: 278, command: 'rule andRight' 
820390     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [195] goal: 4955, source line: 279, command: 'rule andRight' 
820390     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [196] goal: 4957, source line: 280, command: 'tryclose branch' 
820405     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [197] goal: 4958, source line: 281, command: 'rule seqNPermSwapNPerm' 
820406     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [198] goal: 4977, source line: 283, command: 'instantiate hide var=iv with='jv_0'' 
820407     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [199] goal: 4978, source line: 284, command: 'instantiate hide var=jv with='v_x_0'' 
820408     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [200] goal: 4979, source line: 285, command: 'rule impLeft' 
820409     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [201] goal: 4980, source line: 286, command: 'tryclose branch' 
820521     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [202] goal: 4981, source line: 287, command: 'rule seqNPermSwapNPerm formula='seqNPerm(seqSwap(s_0, jv_0, v_x_0))'' 
820521     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [203] goal: 5093, source line: 288, command: 'instantiate hide var=iv with='jv_0'' 
820523     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [204] goal: 5094, source line: 289, command: 'instantiate hide var=jv with='v_y_0'' 
820524     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [205] goal: 5095, source line: 290, command: 'rule impLeft' 
820525     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [206] goal: 5096, source line: 291, command: 'tryclose branch' 
820636     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [207] goal: 5097, source line: 292, command: 'tryclose branch' 
820642     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [208] goal: 4956, source line: 293, command: 'rule allRight' 
820643     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [209] goal: 5212, source line: 295, command: 'rule impRight' 
820644     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [210] goal: 5213, source line: 296, command: 'rule andLeft' 
820645     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [211] goal: 5214, source line: 297, command: 'instantiate var=iv with='v_iv_0'' 
820645     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [212] goal: 5215, source line: 300, command: 'rule impLeft' 
820646     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [213] goal: 5216, source line: 301, command: 'tryclose branch' 
820771     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [214] goal: 5217, source line: 302, command: 'rule getOfSwap' 
820772     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [215] goal: 5337, source line: 304, command: 'rule ifthenelse_negated' 
820773     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [216] goal: 5338, source line: 305, command: 'rule ifthenelse_split occ=0' 
820775     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [217] goal: 5339, source line: 306, command: 'rule andLeft' 
820776     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [218] goal: 5341, source line: 307, command: 'rule andLeft' 
820776     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [219] goal: 5342, source line: 308, command: 'rule andLeft' 
820777     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [220] goal: 5343, source line: 309, command: 'rule ifthenelse_split occ=0' 
820777     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [221] goal: 5344, source line: 310, command: 'rule getOfSwap' 
820778     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [222] goal: 5346, source line: 311, command: 'rule ifthenelse_negated' 
820779     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [223] goal: 5347, source line: 312, command: 'rule ifthenelse_split occ=0' 
820780     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [224] goal: 5348, source line: 313, command: 'rule andLeft' 
820781     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [225] goal: 5350, source line: 314, command: 'rule andLeft' 
820781     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [226] goal: 5351, source line: 315, command: 'rule andLeft' 
820782     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [227] goal: 5352, source line: 316, command: 'rule ifthenelse_split occ=0' 
820783     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [228] goal: 5353, source line: 317, command: 'tryclose branch' 
820892     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [229] goal: 5354, source line: 318, command: 'rule ifthenelse_split occ=0' 
820893     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [230] goal: 5463, source line: 319, command: 'tryclose branch' 
820901     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [231] goal: 5464, source line: 320, command: 'tryclose branch' 
821000     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [232] goal: 5349, source line: 321, command: 'tryclose branch' 
821104     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [233] goal: 5345, source line: 322, command: 'rule ifthenelse_split' 
821106     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [234] goal: 5660, source line: 324, command: 'rule getOfSwap' 
821107     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [235] goal: 5662, source line: 325, command: 'rule ifthenelse_negated' 
821108     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [236] goal: 5663, source line: 326, command: 'rule ifthenelse_split occ=0' 
821109     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [237] goal: 5664, source line: 327, command: 'rule andLeft' 
821109     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [238] goal: 5666, source line: 328, command: 'rule andLeft' 
821110     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [239] goal: 5667, source line: 329, command: 'rule andLeft' 
821110     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [240] goal: 5668, source line: 330, command: 'rule ifthenelse_split occ=0' 
821111     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [241] goal: 5669, source line: 331, command: 'tryclose branch' 
821227     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [242] goal: 5670, source line: 332, command: 'tryclose branch' 
821235     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [243] goal: 5665, source line: 333, command: 'tryclose branch' 
821398     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [244] goal: 5661, source line: 334, command: 'rule getOfSwap' 
821399     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [245] goal: 5887, source line: 336, command: 'rule ifthenelse_negated' 
821400     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [246] goal: 5888, source line: 337, command: 'rule ifthenelse_split occ=0' 
821401     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [247] goal: 5889, source line: 338, command: 'rule andLeft' 
821402     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [248] goal: 5891, source line: 339, command: 'rule andLeft' 
821402     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [249] goal: 5892, source line: 340, command: 'rule andLeft' 
821402     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [250] goal: 5893, source line: 341, command: 'rule ifthenelse_split occ=0' 
821403     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [251] goal: 5894, source line: 342, command: 'tryclose branch' 
821409     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [252] goal: 5895, source line: 343, command: 'rule ifthenelse_split occ=0' 
821410     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [253] goal: 5897, source line: 344, command: 'tryclose branch' 
821513     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [254] goal: 5898, source line: 345, command: 'tryclose branch' 
821520     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [255] goal: 5890, source line: 346, command: 'tryclose branch' 
821527     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [256] goal: 5340, source line: 347, command: 'tryclose branch' 
821654     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [257] goal: 4954, source line: 348, command: 'rule getOfSwap' 
821655     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [258] goal: 6115, source line: 350, command: 'rule ifthenelse_negated' 
821656     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [259] goal: 6116, source line: 351, command: 'rule ifthenelse_split occ=0' 
821657     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [260] goal: 6117, source line: 352, command: 'rule andLeft' 
821657     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [261] goal: 6119, source line: 353, command: 'rule andLeft' 
821658     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [262] goal: 6120, source line: 354, command: 'rule andLeft' 
821658     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [263] goal: 6121, source line: 355, command: 'rule ifthenelse_split occ=0' 
821659     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [264] goal: 6122, source line: 356, command: 'tryclose branch' 
821731     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [265] goal: 6123, source line: 357, command: 'rule ifthenelse_split occ=0' 
821732     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [266] goal: 6193, source line: 358, command: 'rule getOfSwap' 
821733     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [267] goal: 6195, source line: 359, command: 'rule ifthenelse_negated' 
821734     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [268] goal: 6196, source line: 360, command: 'rule ifthenelse_split occ=0' 
821735     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [269] goal: 6197, source line: 361, command: 'tryclose branch' 
821742     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [270] goal: 6198, source line: 362, command: 'tryclose branch' 
821749     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [271] goal: 6194, source line: 363, command: 'tryclose branch' 
821911     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [272] goal: 6118, source line: 364, command: 'tryclose branch' 
822027     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [273] goal: 4952, source line: 365, command: 'rule getOfSwap' 
822028     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [274] goal: 6456, source line: 367, command: 'rule ifthenelse_negated' 
822029     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [275] goal: 6457, source line: 368, command: 'rule ifthenelse_split occ=0' 
822030     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [276] goal: 6458, source line: 369, command: 'tryclose branch' 
822239     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [277] goal: 6459, source line: 370, command: 'tryclose branch' 
822354     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [278] goal: 4949, source line: 371, command: 'cut 'int::seqGet(s_0, v_y_0)=v_x_0'' 
822355     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [279] goal: 6735, source line: 375, command: 'tryclose branch' 
826335     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [280] goal: 6735, source line: 378, command: 'rule seqNPermSwapNPerm' 
826340     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [281] goal: 8783, source line: 380, command: 'instantiate hide var=iv with='jv_1'' 
826341     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [282] goal: 8784, source line: 381, command: 'instantiate hide var=jv with='v_y_0'' 
826342     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [283] goal: 8785, source line: 382, command: 'rule impLeft' 
826343     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [284] goal: 8786, source line: 383, command: 'tryclose branch' 
826487     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [285] goal: 8787, source line: 384, command: 'rule seqNPermSwapNPerm formula='seqNPerm(seqSwap(s_0,jv_1,v_y_0))'' 
826488     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [286] goal: 8909, source line: 385, command: 'instantiate hide var=iv with='jv_1'' 
826489     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [287] goal: 8910, source line: 386, command: 'instantiate hide var=jv with='v_x_0'' 
826490     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [288] goal: 8911, source line: 387, command: 'rule impLeft' 
826492     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [289] goal: 8912, source line: 388, command: 'tryclose branch' 
826623     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [290] goal: 8913, source line: 389, command: 'tryclose branch' 
830493     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [291] goal: 6736, source line: 390, command: 'tryclose branch' 
834698     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [292] goal: 6736, source line: 397, command: 'rule seqNPermSwapNPerm formula='seqNPerm(s_0)'' 
834703     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [293] goal: 12633, source line: 399, command: 'instantiate hide var=iv with='v_x_0'' 
834704     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [294] goal: 12634, source line: 400, command: 'instantiate hide var=jv with='jv_0'' 
834705     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [295] goal: 12635, source line: 401, command: 'rule impLeft' 
834706     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [296] goal: 12636, source line: 402, command: 'tryclose branch' 
834874     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [297] goal: 12637, source line: 403, command: 'rule seqNPermSwapNPerm formula='seqNPerm(seqSwap(s_0,v_x_0,jv_0))'' 
834875     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [298] goal: 12757, source line: 404, command: 'instantiate hide var=iv with='v_y_0'' 
834877     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [299] goal: 12758, source line: 405, command: 'instantiate hide var=jv with='jv_1'' 
834878     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [300] goal: 12759, source line: 406, command: 'instantiate hide var=v_r with='seqSwap(seqSwap(s_0, v_x_0, jv_0), v_y_0, jv_1)' ...' 
834879     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [301] goal: 12760, source line: 407, command: 'tryclose branch' 
836402     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm2/Taclet_schiffl_thm_1.proof 
836402     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 111.6ns 
836403     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
839639     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.24s 
839639     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: schiffl_thm_1 
840688     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: schiffl_thm_1 
840690     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 8.3ns 
840690     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [1] goal: 0, source line: 50, command: 'macro split-prop' 
840698     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [2] goal: 10, source line: 51, command: 'rule schiffl_lemma_2 formula='seqPerm(f_s, f_t)'' 
840710     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [3] goal: 11, source line: 52, command: 'instantiate hide var=x with='f_x'' 
840712     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [4] goal: 12, source line: 53, command: 'instantiate hide var=y with='f_y'' 
840715     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [5] goal: 13, source line: 54, command: 'rule impLeft' 
840717     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [6] goal: 14, source line: 55, command: 'tryclose branch' 
840722     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [7] goal: 15, source line: 56, command: 'rule exLeft' 
840723     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [8] goal: 23, source line: 57, command: 'macro split-prop' 
840728     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [9] goal: 27, source line: 58, command: 'rule seqPermDef occ=1' 
840729     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [10] goal: 28, source line: 59, command: 'rule andRight' 
840732     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [11] goal: 29, source line: 60, command: 'tryclose branch' 
840744     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [12] goal: 30, source line: 61, command: 'instantiate hide var=s with='r_0'' 
840744     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [13] goal: 46, source line: 62, command: 'rule andRight' 
840746     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [14] goal: 47, source line: 63, command: 'tryclose branch' 
840809     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [15] goal: 48, source line: 64, command: 'rule allRight' 
840810     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [16] goal: 119, source line: 65, command: 'rule impRight' 
840811     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [17] goal: 120, source line: 66, command: 'instantiate hide var=iv with='iv_0'' 
840812     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [18] goal: 121, source line: 67, command: 'rule impLeft' 
840812     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [19] goal: 122, source line: 68, command: 'tryclose branch' 
840906     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [20] goal: 123, source line: 69, command: 'rule andLeft' 
840906     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [21] goal: 203, source line: 70, command: 'rule seqNPermRange' 
840907     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [22] goal: 204, source line: 71, command: 'instantiate hide var=iv with='iv_0'' 
840908     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [23] goal: 205, source line: 72, command: 'rule impLeft' 
840909     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [24] goal: 206, source line: 73, command: 'tryclose branch' 
840913     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [25] goal: 207, source line: 74, command: 'rule andLeft' 
840914     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [26] goal: 215, source line: 75, command: 'rule andLeft' 
840914     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [27] goal: 216, source line: 76, command: 'rule seqNPermRange' 
840915     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [28] goal: 217, source line: 77, command: 'instantiate hide var=iv with='f_x'' 
840916     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [29] goal: 218, source line: 78, command: 'rule impLeft' 
840916     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [30] goal: 219, source line: 79, command: 'tryclose branch' 
841022     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [31] goal: 220, source line: 80, command: 'rule andLeft' 
841023     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [32] goal: 311, source line: 81, command: 'rule andLeft' 
841023     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [33] goal: 312, source line: 82, command: 'rule seqNPermRange' 
841024     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [34] goal: 313, source line: 83, command: 'instantiate hide var=iv with='f_y'' 
841025     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [35] goal: 314, source line: 84, command: 'rule impLeft' 
841026     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [36] goal: 315, source line: 85, command: 'tryclose branch' 
841115     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [37] goal: 316, source line: 86, command: 'rule andLeft' 
841116     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [38] goal: 410, source line: 87, command: 'rule andLeft' 
841116     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [39] goal: 411, source line: 88, command: 'rule getOfSeqDef occ=0' 
841117     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [40] goal: 412, source line: 89, command: 'rule getOfSeqDef' 
841117     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [41] goal: 413, source line: 90, command: 'rule ifthenelse_split occ=0' 
841118     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [42] goal: 414, source line: 91, command: 'rule andLeft occ=0' 
841119     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [43] goal: 416, source line: 92, command: 'rule sub_zero_2 occ=0' 
841119     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [44] goal: 417, source line: 93, command: 'rule ifthenelse_split occ=2' 
841120     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [45] goal: 418, source line: 94, command: 'rule andLeft' 
841121     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [46] goal: 420, source line: 95, command: 'rule sub_zero_2 occ=0' 
841121     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [47] goal: 421, source line: 96, command: 'rule add_zero_right occ=0' 
841122     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [48] goal: 422, source line: 97, command: 'rule add_zero_right occ=0' 
841122     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [49] goal: 423, source line: 98, command: 'rule add_zero_right occ=0' 
841123     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [50] goal: 424, source line: 99, command: 'rule add_zero_right occ=0' 
841123     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [51] goal: 425, source line: 100, command: 'rule add_zero_right occ=0' 
841124     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [52] goal: 426, source line: 101, command: 'rule add_zero_right occ=0' 
841124     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [53] goal: 427, source line: 102, command: 'rule ifthenelse_split occ=0' 
841125     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [54] goal: 428, source line: 103, command: 'rule ifthenelse_split occ=0' 
841126     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [55] goal: 430, source line: 104, command: 'tryclose branch' 
841129     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [56] goal: 431, source line: 105, command: 'tryclose branch' 
841167     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [57] goal: 429, source line: 106, command: 'rule ifthenelse_split occ=0' 
841168     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [58] goal: 473, source line: 107, command: 'tryclose branch' 
841297     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [59] goal: 474, source line: 108, command: 'rule ifthenelse_split occ=0' 
841298     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [60] goal: 541, source line: 109, command: 'rule seqNPermInjective' 
841298     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [61] goal: 543, source line: 110, command: 'instantiate hide var=iv with='iv_0'' 
841300     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [62] goal: 544, source line: 111, command: 'instantiate hide var=jv with='f_y'' 
841301     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [63] goal: 545, source line: 112, command: 'rule impLeft' 
841302     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [64] goal: 546, source line: 113, command: 'tryclose branch' 
841354     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [65] goal: 547, source line: 114, command: 'tryclose branch' 
841356     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [66] goal: 542, source line: 115, command: 'rule ifthenelse_split occ=0' 
841357     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [67] goal: 606, source line: 116, command: 'rule seqNPermInjective' 
841358     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [68] goal: 608, source line: 117, command: 'instantiate hide var=iv with='iv_0'' 
841359     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [69] goal: 609, source line: 118, command: 'instantiate hide var=jv with='f_x'' 
841361     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [70] goal: 610, source line: 119, command: 'rule impLeft' 
841361     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [71] goal: 611, source line: 120, command: 'tryclose branch' 
841416     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [72] goal: 612, source line: 121, command: 'tryclose branch' 
841419     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [73] goal: 607, source line: 122, command: 'tryclose branch' 
841422     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [74] goal: 419, source line: 123, command: 'tryclose branch' 
841486     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [75] goal: 415, source line: 124, command: 'tryclose branch' 
841553     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_eqSameSeq.proof 
841553     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 101ns 
841554     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
844717     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.16s 
844717     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: eqSameSeq 
845863     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: eqSameSeq 
845890     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 23.5ms