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

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

tests
0

failures
0

ignored
14m1.32s

duration
100%

successful

Tests

Test Method name Duration Result
powPositive data()[100] 4.086s passed
powPositiveConcrete data()[101] 4.035s passed
powGeq1Concrete data()[102] 4.004s passed
pow2InIntLower data()[103] 4.000s passed
pow2InIntUpper data()[104] 4.061s passed
logSelfConcrete data()[105] 4.120s passed
log1Concrete data()[106] 4.038s passed
logProduct data()[107] 4.021s passed
logTimesBaseConcrete data()[108] 4.067s passed
logProdIdentity data()[109] 4.102s passed
moduloByteIsInByte data()[10] 4.217s passed
logProdIdentityConcrete data()[110] 4.041s passed
logPowIdentity data()[111] 4.062s passed
logPowIdentityConcrete data()[112] 4.054s passed
logPositive data()[113] 4.019s passed
logPositiveConcrete data()[114] 3.975s passed
logMono data()[115] 4.075s passed
logMonoConcrete data()[116] 4.014s passed
powLogLess data()[117] 4.033s passed
powLogMore2 data()[118] 4.029s passed
logLessThanPow data()[119] 4.176s passed
moduloCharIsInChar data()[11] 4.260s passed
logLessThanPowConcrete data()[120] 4.074s passed
logSqueeze data()[121] 4.027s passed
ifthenelse_equals data()[122] 4.019s passed
ifthenelse_equals_1 data()[123] 3.986s passed
ifthenelse_equals_2 data()[124] 3.977s passed
disjointWithSingleton1 data()[125] 4.005s passed
disjointWithSingleton2 data()[126] 4.002s passed
disjointArrayRanges data()[127] 4.048s passed
disjointArrayRangeAllFields1 data()[128] 4.056s passed
disjointArrayRangeAllFields2 data()[129] 4.022s passed
div_unique1 data()[12] 4.447s passed
seqSelfDefinition data()[130] 4.069s passed
seqOutsideValue data()[131] 4.135s passed
castedGetAny data()[132] 4.161s passed
seqGetAlphaCast data()[133] 4.054s passed
getOfSeqSingleton data()[134] 4.212s passed
getOfSeqSingletonConcrete data()[135] 4.089s passed
getOfSeqConcat data()[136] 4.114s passed
getOfSeqSub data()[137] 4.014s passed
getOfSeqReverse data()[138] 4.051s passed
lenOfSeqEmpty data()[139] 4.084s passed
div_unique2 data()[13] 4.299s passed
lenOfSeqSingleton data()[140] 4.101s passed
lenOfSeqConcat data()[141] 4.013s passed
lenOfSeqSub data()[142] 4.138s passed
lenOfSeqReverse data()[143] 4.137s passed
equalityToSeqGetAndSeqLenLeft data()[144] 4.092s passed
equalityToSeqGetAndSeqLenRight data()[145] 4.048s passed
getOfSeqSingletonEQ data()[146] 4.108s passed
getOfSeqConcatEQ data()[147] 4.104s passed
getOfSeqSubEQ data()[148] 4.079s passed
getOfSeqReverseEQ data()[149] 4.122s passed
div_exists data()[14] 4.447s passed
lenOfSeqEmptyEQ data()[150] 4.048s passed
lenOfSeqSingletonEQ data()[151] 3.984s passed
lenOfSeqConcatEQ data()[152] 4.029s passed
lenOfSeqSubEQ data()[153] 4.032s passed
lenOfSeqReverseEQ data()[154] 4.031s passed
getOfSeqDefEQ data()[155] 4.037s passed
lenOfSeqDefEQ data()[156] 4.063s passed
seqConcatWithSeqEmpty1 data()[157] 4.023s passed
seqConcatWithSeqEmpty2 data()[158] 4.159s passed
seqReverseOfSeqEmpty data()[159] 4.214s passed
div_one data()[15] 4.115s passed
subSeqComplete data()[160] 4.087s passed
subSeqTailR data()[161] 4.112s passed
subSeqTailL data()[162] 4.119s passed
subSeqTailEQR data()[163] 4.186s passed
subSeqTailEQL data()[164] 4.147s passed
seqDef_split data()[165] 4.076s passed
seqDef_induction_upper data()[166] 4.106s passed
seqDef_induction_upper_concrete data()[167] 4.139s passed
seqDef_induction_lower data()[168] 4.091s passed
seqDef_induction_lower_concrete data()[169] 4.164s passed
jdiv_one data()[16] 4.158s passed
seqDef_split_in_three data()[170] 4.290s passed
seqDef_empty data()[171] 4.066s passed
seqDef_one_summand data()[172] 4.072s passed
seqDef_lower_equals_upper data()[173] 4.050s passed
seqDefOfSeq data()[174] 4.091s passed
seqSelfDefinitionEQ2 data()[175] 4.052s passed
indexOfSeqSingleton data()[176] 4.087s passed
indexOfSeqConcatFirst data()[177] 4.096s passed
indexOfSeqConcatSecond data()[178] 4.152s passed
indexOfSeqSub data()[179] 4.070s passed
div_zero data()[17] 4.270s passed
lenOfArray2seq data()[180] 4.040s passed
getAnyOfArray2seq data()[181] 4.063s passed
getOfArray2seq data()[182] 4.096s passed
getAnyOfNPermInv data()[183] 4.072s passed
seqNPermRange data()[184] 4.212s passed
seqPermTrans data()[185] 4.120s passed
seqPermRefl data()[186] 4.160s passed
seqPermSplit data()[187] 4.095s passed
seqNPermRight data()[188] 4.403s passed
seqPermFromSwap data()[189] 4.158s passed
divResZero1 data()[18] 4.179s passed
seqPermTransAlt0 data()[190] 4.063s passed
seqPermTransAlt1 data()[191] 4.118s passed
seqPermTransAlt2 data()[192] 4.138s passed
seqPermTransAlt3 data()[193] 4.118s passed
seqPermForall data()[194] 4.190s passed
seqPermExists data()[195] 4.228s passed
schiffl_lemma_2 data()[196] 29.045s passed
schiffl_thm_1 data()[197] 5.235s passed
eqSameSeq data()[198] 4.241s passed
divResZero2 data()[19] 4.111s passed
eqTermCut data()[1] 5.055s passed
divResOne1 data()[20] 4.117s passed
divResOne2 data()[21] 4.082s passed
div_cancel1 data()[22] 4.155s passed
div_cancel2 data()[23] 4.058s passed
divAddMultDenom data()[24] 4.098s passed
divMinus data()[25] 4.291s passed
divMinusDenom data()[26] 4.210s passed
divLeastDPos data()[27] 4.170s passed
divLeastDNeg data()[28] 4.114s passed
divGreatestDPos data()[29] 4.095s passed
equivAllRight data()[2] 4.619s passed
divGreatestDNeg data()[30] 4.088s passed
divIncreasingPos data()[31] 4.168s passed
divIncreasingNeg data()[32] 4.064s passed
jdiv_zero data()[33] 4.089s passed
jdivPulloutMinusNum data()[34] 4.120s passed
jdivPulloutMinusDenom data()[35] 4.149s passed
jdiv_uniquePosPos data()[36] 4.071s passed
jdiv_uniquePosNeg data()[37] 4.081s passed
jdiv_uniqueNegPos data()[38] 4.049s passed
jdiv_uniqueNegNeg data()[39] 4.085s passed
irrflConcrete1 data()[3] 4.793s passed
jdivMultDenom1 data()[40] 4.108s passed
jdivMultDenom2 data()[41] 4.020s passed
mod_geZero data()[42] 4.062s passed
mod_lessDenom data()[43] 4.061s passed
jmod_NumPos data()[44] 4.066s passed
jmod_NumNeg data()[45] 4.010s passed
jmod_geZero data()[46] 4.167s passed
jmodNumZero data()[47] 4.025s passed
jmod_pulloutminusNum data()[48] 4.078s passed
jmod_pulloutminusDenom data()[49] 4.016s passed
irrflConcrete2 data()[4] 4.423s passed
jmodUnique1 data()[50] 4.169s passed
jmodUnique2 data()[51] 4.205s passed
intDivRem data()[52] 4.106s passed
jmodjmod data()[53] 4.157s passed
jmodDivisible data()[54] 4.099s passed
jmodDivisibleRep data()[55] 4.093s passed
jdivAddMultDenom data()[56] 4.383s passed
jmodAltZero data()[57] 4.085s passed
jmodAddMultDenomZero data()[58] 4.029s passed
polyDiv_zero data()[59] 4.045s passed
cancel_gtPos data()[5] 4.375s passed
polyMod_ltdivDenom data()[60] 4.082s passed
bsum_empty data()[61] 4.033s passed
bsum_induction_upper data()[62] 4.012s passed
bsum_induction_lower data()[63] 4.133s passed
bsum_num_of_bounds data()[64] 4.082s passed
bsum_num_of_bounds2 data()[65] 4.002s passed
bsum_induction_upper2 data()[66] 4.015s passed
bsum_induction_upper_concrete data()[67] 4.150s passed
bsum_induction_upper_concrete_2 data()[68] 4.051s passed
bsum_induction_upper2_concrete data()[69] 3.995s passed
cancel_gtNeg data()[6] 4.269s passed
bsum_induction_lower_concrete data()[70] 4.017s passed
bsum_induction_lower2 data()[71] 3.992s passed
bsum_induction_lower2_concrete data()[72] 4.080s passed
bsum_positive data()[73] 4.167s passed
bsum_upper_bound data()[74] 4.152s passed
bsum_lower_bound data()[75] 4.183s passed
bsum_positive_lower_bound_element data()[76] 4.136s passed
bsum_sub_same_index data()[77] 4.223s passed
bsum_less_same_index data()[78] 4.286s passed
bsum_equal_except_one_index data()[79] 4.151s passed
moduloIntIsInInt data()[7] 4.304s passed
bsum_num_of_is_max data()[80] 4.071s passed
bsum_num_of_is_max2 data()[81] 4.151s passed
bsum_num_of_is_max3 data()[82] 4.105s passed
bsum_num_of_is_max4 data()[83] 4.030s passed
bsum_num_of_lt_max data()[84] 4.128s passed
bsum_num_of_lt_max2 data()[85] 4.194s passed
bsum_num_of_lt_max3 data()[86] 4.163s passed
bsum_num_of_lt_max4 data()[87] 4.098s passed
bsum_num_of_gt0 data()[88] 4.074s passed
bsum_num_of_gt0_alt data()[89] 4.079s passed
moduloLongIsInLong data()[8] 4.279s passed
bsum_add_concrete data()[90] 4.109s passed
bprod_all_positive data()[91] 3.999s passed
bprod_split data()[92] 4.037s passed
powConcrete0 data()[93] 4.123s passed
powConcrete1 data()[94] 4.047s passed
powSplitFactor data()[95] 4.016s passed
powAdd data()[96] 3.981s passed
powMono data()[97] 4.001s passed
powMonoConcrete data()[98] 4.060s passed
powMonoConcreteRight data()[99] 4.016s passed
moduloShortIsInShort data()[9] 4.118s passed

Standard output

488        INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src/test/resources/testcase/dummyTrue.key 
522        DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 10.4ms 
838        INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
856        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)

2241       DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for Meta 
2244       DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for Meta 
2250       DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for Meta 
2251       DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for Meta 
4468       DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for JavaBigintExpression 
11686      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 10.85s 
11807      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof dummyTrue.key 
11862      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 41.8ns 
11889      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/firstOrder/Taclet_eqTermCut.proof 
11891      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 1.96ms 
11898      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
15743      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.85s 
15746      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: eqTermCut 
16894      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: eqTermCut 
16927      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 25.07ms 
16939      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/firstOrder/Taclet_equivAllRight.proof 
16939      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 256.6ns 
16941      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
20437      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.5s 
20437      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: equivAllRight 
21528      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: equivAllRight 
21554      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 21.68ms 
21563      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_irrflConcrete1.proof 
21563      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 492.5ns 
21568      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
25086      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.52s 
25087      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: irrflConcrete1 
26341      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: irrflConcrete1 
26350      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.31ms 
26354      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_irrflConcrete2.proof 
26354      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 407.9ns 
26356      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
29677      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.32s 
29678      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: irrflConcrete2 
30766      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: irrflConcrete2 
30773      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.77ms 
30778      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_cancel_gtPos.proof 
30778      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 480.9ns 
30780      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
34046      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.27s 
34047      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: cancel_gtPos 
35087      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: cancel_gtPos 
35150      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 58.96ms 
35155      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_cancel_gtNeg.proof 
35155      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 397.8ns 
35157      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
38362      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.2s 
38362      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: cancel_gtNeg 
39384      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: cancel_gtNeg 
39415      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 27.71ms 
39423      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intRulesIgnoringOF/Taclet_moduloIntIsInInt.proof 
39423      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 175.2ns 
39425      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
42620      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.2s 
42621      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: moduloIntIsInInt 
43716      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: moduloIntIsInInt 
43725      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.19ms 
43727      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intRulesIgnoringOF/Taclet_moduloLongIsInLong.proof 
43727      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 174.1ns 
43728      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
46936      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.21s 
46936      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: moduloLongIsInLong 
48000      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: moduloLongIsInLong 
48004      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 874.81ns 
48006      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intRulesIgnoringOF/Taclet_moduloShortIsInShort.proof 
48006      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 137.9ns 
48007      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
51093      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.09s 
51093      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: moduloShortIsInShort 
52118      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: moduloShortIsInShort 
52122      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 851.3ns 
52125      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intRulesIgnoringOF/Taclet_moduloByteIsInByte.proof 
52126      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 887.41ns 
52128      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
55294      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.17s 
55294      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: moduloByteIsInByte 
56336      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: moduloByteIsInByte 
56340      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 819.81ns 
56344      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intRulesIgnoringOF/Taclet_moduloCharIsInChar.proof 
56346      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 1.94ms 
56348      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
59532      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.18s 
59533      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: moduloCharIsInChar 
60580      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: moduloCharIsInChar 
60592      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 699.6ns 
60604      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_div_unique1.proof 
60605      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 544.7ns 
60606      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
63917      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.31s 
63918      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: div_unique1 
64973      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: div_unique1 
65048      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 69.66ms 
65059      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_div_unique2.proof 
65060      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 1.04ms 
65062      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
68262      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.2s 
68262      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: div_unique2 
69250      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: div_unique2 
69344      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 87.72ms 
69357      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_div_exists.proof 
69357      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 169.8ns 
69359      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
72500      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.14s 
72501      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: div_exists 
73510      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: div_exists 
73796      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 273.69ms 
73800      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_div_one.proof 
73801      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 564.4ns 
73803      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
76914      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.11s 
76915      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: div_one 
77905      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: div_one 
77913      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 5.11ms 
77915      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdiv_one.proof 
77916      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 274.5ns 
77917      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
81014      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.1s 
81015      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdiv_one 
82066      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdiv_one 
82071      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.7ms 
82084      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_div_zero.proof 
82085      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 476.9ns 
82086      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
85266      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.18s 
85267      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: div_zero 
86281      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: div_zero 
86343      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 56.32ms 
86346      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divResZero1.proof 
86347      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 426.8ns 
86348      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
89486      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.14s 
89487      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divResZero1 
90496      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divResZero1 
90521      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 20.49ms 
90524      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divResZero2.proof 
90525      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 397.2ns 
90526      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
93618      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.09s 
93619      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divResZero2 
94605      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divResZero2 
94633      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 24.49ms 
94635      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divResOne1.proof 
94636      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 265.7ns 
94637      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
97715      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.08s 
97716      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divResOne1 
98723      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divResOne1 
98749      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 22.7ms 
98752      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divResOne2.proof 
98752      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 206.8ns 
98753      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
101824     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.07s 
101824     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divResOne2 
102806     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divResOne2 
102831     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 22.49ms 
102834     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_div_cancel1.proof 
102834     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 268ns 
102836     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
105953     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.12s 
105953     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: div_cancel1 
106945     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: div_cancel1 
106987     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 38.11ms 
106989     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_div_cancel2.proof 
106989     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 210.2ns 
106990     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
110049     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.06s 
110050     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: div_cancel2 
111041     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: div_cancel2 
111045     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.73ms 
111047     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divAddMultDenom.proof 
111047     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 108.1ns 
111048     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
114103     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.05s 
114103     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divAddMultDenom 
115072     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divAddMultDenom 
115143     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 64.31ms 
115145     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divMinus.proof 
115145     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 122.1ns 
115146     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
118306     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.16s 
118307     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divMinus 
119343     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divMinus 
119433     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 81.29ms 
119446     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divMinusDenom.proof 
119446     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 385.71ns 
119448     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
122578     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.13s 
122578     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divMinusDenom 
123583     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divMinusDenom 
123652     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 63.03ms 
123660     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divLeastDPos.proof 
123661     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 1.28ms 
123662     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
126818     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.16s 
126818     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divLeastDPos 
127813     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divLeastDPos 
127827     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 10.07ms 
127830     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divLeastDNeg.proof 
127830     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 384.41ns 
127832     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
130913     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.08s 
130914     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divLeastDNeg 
131920     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divLeastDNeg 
131941     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 17.16ms 
131944     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divGreatestDPos.proof 
131944     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 402ns 
131945     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
135024     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.08s 
135025     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divGreatestDPos 
136020     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divGreatestDPos 
136036     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 12.89ms 
136038     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divGreatestDNeg.proof 
136038     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 134.4ns 
136039     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
139127     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.09s 
139128     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divGreatestDNeg 
140110     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divGreatestDNeg 
140124     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 11.94ms 
140126     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divIncreasingPos.proof 
140126     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 97.4ns 
140127     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
143269     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.14s 
143270     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divIncreasingPos 
144282     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divIncreasingPos 
144292     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 7.8ms 
144294     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divIncreasingNeg.proof 
144295     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 299.4ns 
144296     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
147381     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.08s 
147382     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divIncreasingNeg 
148341     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divIncreasingNeg 
148356     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 12.15ms 
148358     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdiv_zero.proof 
148359     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 278.6ns 
148360     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
151454     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.09s 
151454     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdiv_zero 
152441     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdiv_zero 
152446     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.12ms 
152447     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdivPulloutMinusNum.proof 
152447     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 91.3ns 
152448     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
155580     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.13s 
155580     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdivPulloutMinusNum 
156546     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdivPulloutMinusNum 
156565     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 15.87ms 
156567     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdivPulloutMinusDenom.proof 
156567     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 121.4ns 
156568     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
159627     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.06s 
159627     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdivPulloutMinusDenom 
160591     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdivPulloutMinusDenom 
160712     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 112.51ms 
160717     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdiv_uniquePosPos.proof 
160720     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 3.23ms 
160722     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
163754     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.03s 
163754     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdiv_uniquePosPos 
164753     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdiv_uniquePosPos 
164784     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 26.63ms 
164787     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdiv_uniquePosNeg.proof 
164787     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 178.3ns 
164789     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
167833     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.04s 
167834     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdiv_uniquePosNeg 
168840     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdiv_uniquePosNeg 
168867     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 23.4ms 
168868     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdiv_uniqueNegPos.proof 
168868     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 171.3ns 
168869     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
171889     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.02s 
171889     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdiv_uniqueNegPos 
172890     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdiv_uniqueNegPos 
172915     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 21.77ms 
172916     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdiv_uniqueNegNeg.proof 
172917     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 111.4ns 
172918     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
175974     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.06s 
175974     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdiv_uniqueNegNeg 
176969     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdiv_uniqueNegNeg 
177000     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 27.02ms 
177002     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdivMultDenom1.proof 
177002     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 95.4ns 
177003     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
180020     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.02s 
180021     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdivMultDenom1 
181044     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdivMultDenom1 
181108     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 57.36ms 
181111     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdivMultDenom2.proof 
181111     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 384.9ns 
181113     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
184138     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.03s 
184139     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdivMultDenom2 
185121     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdivMultDenom2 
185128     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.7ms 
185131     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_mod_geZero.proof 
185131     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 212ns 
185132     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
188185     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.05s 
188186     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: mod_geZero 
189183     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: mod_geZero 
189190     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.86ms 
189192     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_mod_lessDenom.proof 
189192     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 297.5ns 
189194     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
192295     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.1s 
192296     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: mod_lessDenom 
193240     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: mod_lessDenom 
193252     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 9.48ms 
193259     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmod_NumPos.proof 
193259     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 177.1ns 
193260     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
196332     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.07s 
196332     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmod_NumPos 
197308     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmod_NumPos 
197323     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 11.28ms 
197324     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmod_NumNeg.proof 
197324     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 108.5ns 
197326     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
200326     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3s 
200327     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmod_NumNeg 
201301     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmod_NumNeg 
201332     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 27.81ms 
201334     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmod_geZero.proof 
201334     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 98.2ns 
201335     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
204493     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.16s 
204493     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmod_geZero 
205487     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmod_geZero 
205500     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 9.42ms 
205501     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmodNumZero.proof 
205501     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 86.8ns 
205502     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
208524     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.02s 
208525     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmodNumZero 
209519     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmodNumZero 
209523     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.2ms 
209526     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmod_pulloutminusNum.proof 
209526     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 315.9ns 
209528     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
212570     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.04s 
212572     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmod_pulloutminusNum 
213596     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmod_pulloutminusNum 
213602     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.54ms 
213604     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmod_pulloutminusDenom.proof 
213604     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 98.3ns 
213605     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
216623     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.02s 
216624     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmod_pulloutminusDenom 
217610     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmod_pulloutminusDenom 
217618     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.74ms 
217619     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmodUnique1.proof 
217620     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 100.1ns 
217621     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
220660     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.04s 
220660     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmodUnique1 
221657     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmodUnique1 
221786     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 118.47ms 
221790     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmodUnique2.proof 
221790     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 340.9ns 
221792     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
224823     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.03s 
224824     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmodUnique2 
225864     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmodUnique2 
225991     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 116.47ms 
225994     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_intDivRem.proof 
225994     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 242.2ns 
225995     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
229103     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.11s 
229103     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: intDivRem 
230094     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: intDivRem 
230099     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.44ms 
230100     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmodjmod.proof 
230100     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 100.5ns 
230102     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
233190     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.09s 
233191     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmodjmod 
234194     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmodjmod 
234254     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 56.3ms 
234258     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmodDivisible.proof 
234258     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 485.6ns 
234259     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
237331     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.07s 
237331     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmodDivisible 
238310     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmodDivisible 
238354     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 40.32ms 
238356     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmodDivisibleRep.proof 
238356     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 102.3ns 
238357     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
241466     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.11s 
241466     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmodDivisibleRep 
242444     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmodDivisibleRep 
242447     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.7ms 
242449     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdivAddMultDenom.proof 
242449     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 74.1ns 
242451     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
245546     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.1s 
245547     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdivAddMultDenom 
246512     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdivAddMultDenom 
246828     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 265.01ms 
246832     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmodAltZero.proof 
246833     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 396.8ns 
246834     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
249873     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.04s 
249874     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmodAltZero 
250898     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmodAltZero 
250915     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 14.99ms 
250917     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmodAddMultDenomZero.proof 
250917     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 83.2ns 
250918     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
253941     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.02s 
253941     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmodAddMultDenomZero 
254929     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmodAddMultDenomZero 
254944     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 12.92ms 
254947     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_polyDiv_zero.proof 
254947     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 106.7ns 
254948     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
257975     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.03s 
257975     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: polyDiv_zero 
258966     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: polyDiv_zero 
258990     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 21.08ms 
258992     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_polyMod_ltdivDenom.proof 
258992     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 86.8ns 
258993     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
262050     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.06s 
262050     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: polyMod_ltdivDenom 
263054     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: polyMod_ltdivDenom 
263072     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 10.26ms 
263074     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_empty.proof 
263074     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 75.7ns 
263075     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
266113     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.04s 
266113     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_empty 
267096     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_empty 
267105     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.39ms 
267107     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_induction_upper.proof 
267107     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 242.9ns 
267109     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
270131     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.02s 
270132     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_upper 
271111     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_induction_upper 
271117     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.79ms 
271119     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_induction_lower.proof 
271119     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 122.5ns 
271120     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
274188     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.07s 
274188     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_lower 
275206     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_induction_lower 
275249     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 38.32ms 
275253     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_bounds.proof 
275253     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 291.4ns 
275254     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
278348     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.09s 
278349     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_bounds 
279304     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_bounds 
279332     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 24.69ms 
279334     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_bounds2.proof 
279334     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 101.7ns 
279335     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
282356     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.02s 
282357     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_bounds2 
283308     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_bounds2 
283331     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 19.74ms 
283336     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_induction_upper2.proof 
283337     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 340.4ns 
283338     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
286374     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.04s 
286375     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_upper2 
287345     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_induction_upper2 
287350     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.24ms 
287351     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_induction_upper_concrete.proof 
287351     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 97.5ns 
287352     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
290493     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.14s 
290493     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_upper_concrete 
291492     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_induction_upper_concrete 
291499     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.61ms 
291501     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_induction_upper_concrete_2.proof 
291501     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 180ns 
291502     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
294543     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.04s 
294544     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_upper_concrete_2 
295543     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_induction_upper_concrete_2 
295550     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 5.28ms 
295552     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_induction_upper2_concrete.proof 
295552     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 86.6ns 
295553     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
298575     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.02s 
298575     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_upper2_concrete 
299541     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_induction_upper2_concrete 
299546     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.12ms 
299547     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_induction_lower_concrete.proof 
299547     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 82.4ns 
299548     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
302570     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.02s 
302571     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_lower_concrete 
303559     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_induction_lower_concrete 
303562     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 938.9ns 
303563     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_induction_lower2.proof 
303563     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 69.2ns 
303564     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
306555     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.99s 
306556     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_lower2 
307548     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_induction_lower2 
307554     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.51ms 
307555     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_induction_lower2_concrete.proof 
307555     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 85.4ns 
307556     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
310645     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.09s 
310646     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_lower2_concrete 
311631     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_induction_lower2_concrete 
311634     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.29ms 
311635     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_positive.proof 
311635     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 73ns 
311636     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
314676     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.04s 
314677     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_positive 
315716     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_positive 
315801     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 81.75ms 
315804     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_upper_bound.proof 
315804     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 90.3ns 
315805     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
318853     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.05s 
318854     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_upper_bound 
319873     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_upper_bound 
319953     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 75.2ms 
319955     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_lower_bound.proof 
319956     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 228.6ns 
319957     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
323087     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.13s 
323087     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_lower_bound 
324081     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_lower_bound 
324136     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 51.53ms 
324138     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_positive_lower_bound_element.proof 
324138     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 68.2ns 
324139     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
327244     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.11s 
327245     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_positive_lower_bound_element 
328192     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_positive_lower_bound_element 
328272     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 75.37ms 
328274     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_sub_same_index.proof 
328274     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 128.8ns 
328275     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
331373     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.1s 
331374     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_sub_same_index 
332396     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_sub_same_index 
332495     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 94.84ms 
332497     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_less_same_index.proof 
332497     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 70.4ns 
332498     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
335647     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.15s 
335647     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_less_same_index 
336691     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_less_same_index 
336780     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 82.07ms 
336783     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_equal_except_one_index.proof 
336783     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 92.7ns 
336784     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
339885     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.1s 
339885     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_equal_except_one_index 
340891     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_equal_except_one_index 
340932     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 37.19ms 
340933     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_is_max.proof 
340934     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 89.8ns 
340934     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
343994     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.06s 
343994     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_is_max 
344964     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_is_max 
345003     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 35.76ms 
345005     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_is_max2.proof 
345005     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 94.4ns 
345006     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
348042     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.04s 
348043     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_is_max2 
349102     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_is_max2 
349154     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 48.26ms 
349158     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_is_max3.proof 
349158     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 90.8ns 
349159     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
352241     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.08s 
352241     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_is_max3 
353231     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_is_max3 
353260     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 26.28ms 
353262     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_is_max4.proof 
353262     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 79.8ns 
353263     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
356254     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.99s 
356254     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_is_max4 
357236     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_is_max4 
357289     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 48.75ms 
357292     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_lt_max.proof 
357292     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 266.3ns 
357293     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
360388     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.09s 
360389     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_lt_max 
361367     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_lt_max 
361418     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 46.99ms 
361420     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_lt_max2.proof 
361420     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 105.7ns 
361421     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
364572     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.15s 
364573     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_lt_max2 
365572     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_lt_max2 
365612     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 35.83ms 
365614     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_lt_max3.proof 
365614     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 79.5ns 
365615     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
368769     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.15s 
368769     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_lt_max3 
369724     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_lt_max3 
369775     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 47.14ms 
369777     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_lt_max4.proof 
369778     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 1.02ms 
369779     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
372819     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.04s 
372819     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_lt_max4 
373832     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_lt_max4 
373873     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 35.05ms 
373876     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_gt0.proof 
373877     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 412.2ns 
373878     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
376935     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.06s 
376936     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_gt0 
377906     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_gt0 
377948     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 37.98ms 
377950     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_gt0_alt.proof 
377950     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 98.8ns 
377951     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
380973     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.02s 
380973     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_gt0_alt 
381979     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_gt0_alt 
382027     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 44.25ms 
382030     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_add_concrete.proof 
382030     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 268.9ns 
382031     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
385156     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.12s 
385156     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_add_concrete 
386126     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_add_concrete 
386136     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 7.82ms 
386137     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bprod/Taclet_bprod_all_positive.proof 
386137     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 68.1ns 
386138     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
389116     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.98s 
389117     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bprod_all_positive 
390109     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bprod_all_positive 
390135     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 21.88ms 
390139     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bprod/Taclet_bprod_split.proof 
390139     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 253.2ns 
390140     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
393197     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.06s 
393198     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bprod_split 
394169     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bprod_split 
394175     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.88ms 
394176     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powConcrete0.proof 
394176     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 88.5ns 
394177     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
397289     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.11s 
397290     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powConcrete0 
398293     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powConcrete0 
398298     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.17ms 
398301     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powConcrete1.proof 
398301     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 264.3ns 
398302     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
401332     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.03s 
401332     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powConcrete1 
402341     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powConcrete1 
402344     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.05ms 
402346     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powSplitFactor.proof 
402346     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 79.3ns 
402347     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
405388     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.04s 
405388     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powSplitFactor 
406350     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powSplitFactor 
406361     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 8.12ms 
406363     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powAdd.proof 
406363     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 108ns 
406364     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
409386     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.02s 
409386     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powAdd 
410334     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powAdd 
410342     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 6.15ms 
410344     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powMono.proof 
410344     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 59.5ns 
410345     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
413385     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.04s 
413385     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powMono 
414326     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powMono 
414343     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 15.18ms 
414345     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powMonoConcrete.proof 
414345     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 76.3ns 
414346     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
417394     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.05s 
417394     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powMonoConcrete 
418399     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powMonoConcrete 
418403     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.56ms 
418406     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powMonoConcreteRight.proof 
418406     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 262.6ns 
418407     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
421423     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.02s 
421423     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powMonoConcreteRight 
422416     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powMonoConcreteRight 
422419     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 840.71ns 
422421     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powPositive.proof 
422421     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 74.8ns 
422422     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
425464     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.04s 
425464     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powPositive 
426494     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powPositive 
426505     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 5.82ms 
426507     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powPositiveConcrete.proof 
426507     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 69.1ns 
426507     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
429532     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.02s 
429532     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powPositiveConcrete 
430538     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powPositiveConcrete 
430541     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 781ns 
430542     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powGeq1Concrete.proof 
430542     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 56.8ns 
430543     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
433569     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.03s 
433569     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powGeq1Concrete 
434542     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powGeq1Concrete 
434544     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 689.5ns 
434546     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_pow2InIntLower.proof 
434546     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 59.7ns 
434547     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
437553     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.01s 
437553     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: pow2InIntLower 
438542     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: pow2InIntLower 
438544     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 804.21ns 
438546     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_pow2InIntUpper.proof 
438546     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 60.3ns 
438547     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
441568     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.02s 
441568     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: pow2InIntUpper 
442598     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: pow2InIntUpper 
442605     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.67ms 
442606     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logSelfConcrete.proof 
442606     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 57.9ns 
442607     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
445720     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.11s 
445720     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logSelfConcrete 
446713     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logSelfConcrete 
446726     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 9.99ms 
446727     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_log1Concrete.proof 
446727     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 79.5ns 
446728     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
449784     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.06s 
449784     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: log1Concrete 
450757     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: log1Concrete 
450762     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.3ms 
450764     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logProduct.proof 
450764     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 168.9ns 
450765     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
453797     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.03s 
453798     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logProduct 
454773     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logProduct 
454785     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 8.69ms 
454786     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logTimesBaseConcrete.proof 
454786     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 68.4ns 
454787     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
457892     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.1s 
457892     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logTimesBaseConcrete 
458845     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logTimesBaseConcrete 
458851     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.89ms 
458853     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logProdIdentity.proof 
458853     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 73.1ns 
458854     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
461951     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.1s 
461951     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logProdIdentity 
462930     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logProdIdentity 
462953     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 19.83ms 
462954     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logProdIdentityConcrete.proof 
462954     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 87.6ns 
462955     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
465998     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.04s 
465998     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logProdIdentityConcrete 
466989     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logProdIdentityConcrete 
466994     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.77ms 
466996     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logPowIdentity.proof 
466996     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 71.9ns 
466997     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
470025     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.03s 
470026     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logPowIdentity 
471052     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logPowIdentity 
471056     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.87ms 
471058     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logPowIdentityConcrete.proof 
471058     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 88.9ns 
471059     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
474119     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.06s 
474119     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logPowIdentityConcrete 
475104     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logPowIdentityConcrete 
475110     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.25ms 
475111     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logPositive.proof 
475111     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 57.2ns 
475112     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
478125     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.01s 
478125     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logPositive 
479103     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logPositive 
479129     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 22.82ms 
479131     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logPositiveConcrete.proof 
479131     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 74.3ns 
479132     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
482123     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.99s 
482123     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logPositiveConcrete 
483097     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logPositiveConcrete 
483103     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 652.41ns 
483106     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logMono.proof 
483106     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 81.2ns 
483107     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
486140     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.03s 
486140     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logMono 
487121     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logMono 
487179     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 52.77ms 
487181     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logMonoConcrete.proof 
487181     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 90ns 
487182     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
490189     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.01s 
490189     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logMonoConcrete 
491189     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logMonoConcrete 
491194     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.59ms 
491195     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powLogLess.proof 
491195     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 61.3ns 
491196     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
494227     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.03s 
494228     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powLogLess 
495192     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powLogLess 
495226     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 29.75ms 
495229     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powLogMore2.proof 
495229     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 232ns 
495230     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
498280     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.05s 
498281     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powLogMore2 
499219     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powLogMore2 
499254     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 31.8ms 
499256     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logLessThanPow.proof 
499256     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 93.9ns 
499257     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
502360     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.1s 
502360     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logLessThanPow 
503384     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logLessThanPow 
503431     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 37.93ms 
503433     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logLessThanPowConcrete.proof 
503433     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 120.3ns 
503434     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
506512     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.08s 
506512     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logLessThanPowConcrete 
507502     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logLessThanPowConcrete 
507505     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.1ms 
507507     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logSqueeze.proof 
507507     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 78.5ns 
507508     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
510523     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.02s 
510523     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logSqueeze 
511524     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logSqueeze 
511532     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 5.56ms 
511533     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/booleanRules/Taclet_ifthenelse_equals.proof 
511533     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 55.9ns 
511534     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
514572     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.04s 
514572     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: ifthenelse_equals 
515547     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: ifthenelse_equals 
515551     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.77ms 
515552     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/booleanRules/Taclet_ifthenelse_equals_1.proof 
515552     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 76.4ns 
515553     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
518556     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3s 
518556     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: ifthenelse_equals_1 
519532     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: ifthenelse_equals_1 
519537     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.56ms 
519540     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/booleanRules/Taclet_ifthenelse_equals_2.proof 
519540     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 66.7ns 
519541     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
522525     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.98s 
522525     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: ifthenelse_equals_2 
523513     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: ifthenelse_equals_2 
523516     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.29ms 
523518     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/locSet/Taclet_disjointWithSingleton1.proof 
523518     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 55.9ns 
523519     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
526513     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.99s 
526513     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: disjointWithSingleton1 
527516     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: disjointWithSingleton1 
527522     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.51ms 
527523     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/locSet/Taclet_disjointWithSingleton2.proof 
527523     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 99.1ns 
527524     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
530517     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.99s 
530517     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: disjointWithSingleton2 
531520     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: disjointWithSingleton2 
531523     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.71ms 
531525     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/locSet/Taclet_disjointArrayRanges.proof 
531525     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 59.3ns 
531526     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
534591     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.07s 
534591     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: disjointArrayRanges 
535558     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: disjointArrayRanges 
535571     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 10.6ms 
535573     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/locSet/Taclet_disjointArrayRangeAllFields1.proof 
535573     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 57.4ns 
535574     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
538633     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.06s 
538634     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: disjointArrayRangeAllFields1 
539608     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: disjointArrayRangeAllFields1 
539627     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 17.05ms 
539629     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/locSet/Taclet_disjointArrayRangeAllFields2.proof 
539629     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 88.2ns 
539630     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
542633     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3s 
542633     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: disjointArrayRangeAllFields2 
543627     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: disjointArrayRangeAllFields2 
543648     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 18.3ms 
543652     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqSelfDefinition.proof 
543652     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 296.4ns 
543653     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
546675     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.02s 
546675     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqSelfDefinition 
547699     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqSelfDefinition 
547718     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 16.63ms 
547719     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqOutsideValue.proof 
547720     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 71.4ns 
547720     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
550823     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.1s 
550824     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqOutsideValue 
551846     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqOutsideValue 
551853     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.93ms 
551855     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_castedGetAny.proof 
551855     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 78.2ns 
551856     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
554955     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.1s 
554955     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: castedGetAny 
556004     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: castedGetAny 
556014     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 7.28ms 
556015     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqGetAlphaCast.proof 
556015     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 74.1ns 
556016     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
559048     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.03s 
559048     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqGetAlphaCast 
560064     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqGetAlphaCast 
560067     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.13ms 
560069     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqSingleton.proof 
560069     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 88.5ns 
560070     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
563254     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.18s 
563254     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqSingleton 
564277     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqSingleton 
564281     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.05ms 
564282     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqSingletonConcrete.proof 
564282     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 72.3ns 
564283     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
567346     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.06s 
567346     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqSingletonConcrete 
568366     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqSingletonConcrete 
568369     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.18ms 
568371     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqConcat.proof 
568371     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 65.8ns 
568372     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
571413     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.04s 
571413     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqConcat 
572462     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqConcat 
572482     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 18.18ms 
572485     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqSub.proof 
572485     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 84.5ns 
572486     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
575492     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.01s 
575492     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqSub 
576492     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqSub 
576498     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.68ms 
576501     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqReverse.proof 
576502     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 287.6ns 
576504     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
579532     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.03s 
579532     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqReverse 
580542     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqReverse 
580551     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 6.74ms 
580552     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqEmpty.proof 
580552     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 67.6ns 
580553     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
583627     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.07s 
583627     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqEmpty 
584631     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqEmpty 
584635     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.29ms 
584636     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqSingleton.proof 
584636     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 139.6ns 
584637     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
587698     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.06s 
587698     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqSingleton 
588732     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqSingleton 
588735     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 977.11ns 
588737     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqConcat.proof 
588737     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 73ns 
588738     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
591750     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.01s 
591750     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqConcat 
592743     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqConcat 
592748     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.3ms 
592751     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqSub.proof 
592751     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 266.2ns 
592752     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
595884     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.13s 
595884     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqSub 
596882     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqSub 
596886     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.89ms 
596887     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqReverse.proof 
596888     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 68.4ns 
596888     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
600033     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.14s 
600033     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqReverse 
601018     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqReverse 
601023     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.33ms 
601024     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_equalityToSeqGetAndSeqLenLeft.proof 
601024     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 58ns 
601025     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
604072     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.05s 
604072     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: equalityToSeqGetAndSeqLenLeft 
605111     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: equalityToSeqGetAndSeqLenLeft 
605115     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.88ms 
605116     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_equalityToSeqGetAndSeqLenRight.proof 
605117     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 89.8ns 
605117     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
608147     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.03s 
608147     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: equalityToSeqGetAndSeqLenRight 
609156     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: equalityToSeqGetAndSeqLenRight 
609164     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 5.94ms 
609165     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqSingletonEQ.proof 
609165     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 77.5ns 
609166     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
612296     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.13s 
612296     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqSingletonEQ 
613267     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqSingletonEQ 
613271     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.88ms 
613273     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqConcatEQ.proof 
613273     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 62.3ns 
613274     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
616336     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.06s 
616336     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqConcatEQ 
617358     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqConcatEQ 
617375     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 14.43ms 
617377     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqSubEQ.proof 
617377     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 103.7ns 
617378     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
620447     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.07s 
620447     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqSubEQ 
621451     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqSubEQ 
621455     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.19ms 
621456     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqReverseEQ.proof 
621456     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 103.2ns 
621457     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
624532     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.08s 
624532     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqReverseEQ 
625566     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqReverseEQ 
625576     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 8.09ms 
625578     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqEmptyEQ.proof 
625578     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 88ns 
625579     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
628606     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.03s 
628606     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqEmptyEQ 
629621     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqEmptyEQ 
629625     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.37ms 
629626     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqSingletonEQ.proof 
629626     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 67.3ns 
629627     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
632607     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.98s 
632607     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqSingletonEQ 
633605     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqSingletonEQ 
633609     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.22ms 
633610     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqConcatEQ.proof 
633610     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 71.9ns 
633611     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
636615     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3s 
636615     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqConcatEQ 
637630     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqConcatEQ 
637637     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 5.36ms 
637639     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqSubEQ.proof 
637639     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 73.6ns 
637640     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
640654     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.01s 
640654     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqSubEQ 
641664     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqSubEQ 
641670     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.84ms 
641671     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqReverseEQ.proof 
641671     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 64.2ns 
641672     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
644675     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3s 
644675     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqReverseEQ 
645695     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqReverseEQ 
645700     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.88ms 
645701     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqDefEQ.proof 
645701     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 68.7ns 
645702     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
648772     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.07s 
648772     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqDefEQ 
649728     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqDefEQ 
649734     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.8ms 
649740     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqDefEQ.proof 
649740     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 61.8ns 
649741     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
652776     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.03s 
652776     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqDefEQ 
653788     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqDefEQ 
653802     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 11.76ms 
653806     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqConcatWithSeqEmpty1.proof 
653806     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 234.9ns 
653807     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
656776     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.97s 
656776     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqConcatWithSeqEmpty1 
657805     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqConcatWithSeqEmpty1 
657826     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 18.59ms 
657829     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqConcatWithSeqEmpty2.proof 
657829     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 100ns 
657830     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
660936     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.11s 
660936     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqConcatWithSeqEmpty2 
661960     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqConcatWithSeqEmpty2 
661986     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 23.08ms 
661988     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqReverseOfSeqEmpty.proof 
661988     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 78.4ns 
661989     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
665133     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.14s 
665133     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqReverseOfSeqEmpty 
666183     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqReverseOfSeqEmpty 
666200     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 14.13ms 
666202     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_subSeqComplete.proof 
666202     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 72.6ns 
666203     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
669274     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.07s 
669274     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: subSeqComplete 
670272     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: subSeqComplete 
670288     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 13.05ms 
670289     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_subSeqTailR.proof 
670289     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 84.3ns 
670290     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
673317     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.03s 
673317     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: subSeqTailR 
674358     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: subSeqTailR 
674399     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 37.04ms 
674401     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_subSeqTailL.proof 
674401     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 75.1ns 
674402     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
677484     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.08s 
677484     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: subSeqTailL 
678480     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: subSeqTailL 
678518     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 34.88ms 
678519     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_subSeqTailEQR.proof 
678520     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 106.3ns 
678520     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
681582     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.06s 
681582     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: subSeqTailEQR 
682665     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: subSeqTailEQR 
682704     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 35.49ms 
682706     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_subSeqTailEQL.proof 
682706     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 75.8ns 
682707     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
685807     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.1s 
685807     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: subSeqTailEQL 
686826     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: subSeqTailEQL 
686851     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 22.3ms 
686853     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDef_split.proof 
686853     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 82.6ns 
686854     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
689864     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.01s 
689865     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_split 
690877     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDef_split 
690927     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 46.42ms 
690929     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDef_induction_upper.proof 
690929     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 59.3ns 
690930     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
693944     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.01s 
693945     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_induction_upper 
694955     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDef_induction_upper 
695033     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 74.06ms 
695035     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDef_induction_upper_concrete.proof 
695035     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 83.8ns 
695036     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
698110     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.07s 
698110     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_induction_upper_concrete 
699112     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDef_induction_upper_concrete 
699172     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 56.67ms 
699174     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDef_induction_lower.proof 
699174     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 75.1ns 
699175     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
702228     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.05s 
702228     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_induction_lower 
703201     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDef_induction_lower 
703263     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 56.88ms 
703265     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDef_induction_lower_concrete.proof 
703265     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 107.3ns 
703266     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
706333     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.07s 
706333     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_induction_lower_concrete 
707358     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDef_induction_lower_concrete 
707427     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 64.35ms 
707428     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDef_split_in_three.proof 
707428     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 71ns 
707429     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
710500     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.07s 
710501     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_split_in_three 
711504     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDef_split_in_three 
711717     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 203.78ms 
711719     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDef_empty.proof 
711719     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 54.7ns 
711720     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
714752     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.03s 
714753     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_empty 
715772     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDef_empty 
715782     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 8.59ms 
715784     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDef_one_summand.proof 
715784     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 56.8ns 
715785     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
718844     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.06s 
718844     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_one_summand 
719845     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDef_one_summand 
719855     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 7.91ms 
719857     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDef_lower_equals_upper.proof 
719857     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 384.9ns 
719858     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
722886     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.03s 
722886     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_lower_equals_upper 
723898     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDef_lower_equals_upper 
723906     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 5.21ms 
723907     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDefOfSeq.proof 
723907     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 82.1ns 
723908     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
726950     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.04s 
726950     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDefOfSeq 
727964     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDefOfSeq 
727996     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 28.55ms 
727998     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqSelfDefinitionEQ2.proof 
727998     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 58ns 
727999     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
731028     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.03s 
731028     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqSelfDefinitionEQ2 
732027     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqSelfDefinitionEQ2 
732047     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 17.28ms 
732049     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_indexOfSeqSingleton.proof 
732050     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 75.2ns 
732050     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
735129     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.08s 
735130     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: indexOfSeqSingleton 
736132     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: indexOfSeqSingleton 
736136     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.41ms 
736137     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_indexOfSeqConcatFirst.proof 
736137     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 79ns 
736138     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
739203     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.06s 
739203     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: indexOfSeqConcatFirst 
740207     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: indexOfSeqConcatFirst 
740231     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 20.71ms 
740233     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_indexOfSeqConcatSecond.proof 
740233     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 98.1ns 
740234     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
743307     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.07s 
743308     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: indexOfSeqConcatSecond 
744353     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: indexOfSeqConcatSecond 
744384     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 26.44ms 
744385     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_indexOfSeqSub.proof 
744386     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 63.2ns 
744386     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
747418     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.03s 
747418     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: indexOfSeqSub 
748421     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: indexOfSeqSub 
748454     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 29.46ms 
748456     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfArray2seq.proof 
748456     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 80ns 
748457     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
751464     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.01s 
751464     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfArray2seq 
752490     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfArray2seq 
752494     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.83ms 
752495     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getAnyOfArray2seq.proof 
752495     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 60.9ns 
752496     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
755523     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.03s 
755523     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getAnyOfArray2seq 
756552     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getAnyOfArray2seq 
756558     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.31ms 
756559     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfArray2seq.proof 
756559     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 57.4ns 
756560     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
759633     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.07s 
759634     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfArray2seq 
760645     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfArray2seq 
760653     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 6.82ms 
760655     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_getAnyOfNPermInv.proof 
760655     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 125ns 
760656     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
763688     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.03s 
763688     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getAnyOfNPermInv 
764715     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getAnyOfNPermInv 
764725     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 7.61ms 
764727     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqNPermRange.proof 
764727     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 110.9ns 
764728     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
767799     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.07s 
767799     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqNPermRange 
768831     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqNPermRange 
768937     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 99.39ms 
768939     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermTrans.proof 
768939     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 81.9ns 
768940     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
772012     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.07s 
772012     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermTrans 
773012     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermTrans 
773057     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 41.62ms 
773059     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermRefl.proof 
773059     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 80.9ns 
773060     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
776154     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.09s 
776155     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermRefl 
777173     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermRefl 
777217     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 41.3ms 
777220     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermSplit.proof 
777221     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 857.51ns 
777222     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
780262     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.04s 
780262     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermSplit 
781311     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermSplit 
781313     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 420.7ns 
781320     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqNPermRight.proof 
781320     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 194.4ns 
781322     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
784356     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.03s 
784356     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqNPermRight 
785389     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqNPermRight 
785716     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 308.31ms 
785718     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermFromSwap.proof 
785718     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 75.1ns 
785719     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
788772     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.05s 
788772     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermFromSwap 
789796     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermFromSwap 
789874     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 72.44ms 
789875     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermTransAlt0.proof 
789876     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 71.3ns 
789876     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
792920     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.04s 
792920     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermTransAlt0 
793934     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermTransAlt0 
793937     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 502.5ns 
793938     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermTransAlt1.proof 
793938     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 55.6ns 
793939     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
797003     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.06s 
797005     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermTransAlt1 
798052     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermTransAlt1 
798055     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 552ns 
798057     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermTransAlt2.proof 
798057     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 96.3ns 
798058     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
801110     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.05s 
801110     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermTransAlt2 
802189     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermTransAlt2 
802193     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 495ns 
802194     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermTransAlt3.proof 
802194     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 55.7ns 
802195     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
805327     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.13s 
805327     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermTransAlt3 
806309     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermTransAlt3 
806312     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 746.3ns 
806313     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermForall.proof 
806313     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 90.1ns 
806314     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
809350     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.04s 
809351     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermForall 
810360     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermForall 
810477     INFO  Test worker     d.u.i.k.s.SMTFocusResults Analyzing unsat core: (L_1 L_3 L_4) 
810500     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 137.46ms 
810504     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermExists.proof 
810504     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 238.6ns 
810507     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
813622     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.12s 
813622     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermExists 
814656     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermExists 
814729     INFO  Test worker     d.u.i.k.s.SMTFocusResults Analyzing unsat core: (L_1 L_3 L_5 L_6 L_7) 
814731     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 71.56ms 
814732     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm2/Taclet_schiffl_lemma_2.proof 
814732     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 58.7ns 
814735     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
817807     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.07s 
817807     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: schiffl_lemma_2 
818842     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: schiffl_lemma_2 
818844     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 10.8ns 
818892     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 1: 'macro split-prop' 
818960     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 2: 'rule allRight' 
818985     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 3: 'rule allRight' 
818991     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 4: 'macro split-prop' 
819000     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 5: 'rule 'seqPermDefLeft'' 
819004     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 6: 'rule 'andLeft'' 
819005     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 7: 'rule 'exLeft'' 
819008     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 8: 'macro split-prop' 
819012     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 9: 'rule  seqNPermRange' 
819015     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 10: 'instantiate var=iv with='v_x_0' occ=1' 
819018     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 11: 'rule impLeft' 
819020     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 12: 'tryclose branch' 
819286     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 13: 'rule andLeft' 
819288     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 14: 'rule andLeft' 
819290     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 15: 'instantiate var=iv with='v_y_0' occ=1' 
819292     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 16: 'rule impLeft' 
819293     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 17: 'tryclose branch' 
819511     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 18: 'rule andLeft' 
819512     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 19: 'rule andLeft' 
819516     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 20: 'rule seqNPermDefLeft' 
819518     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 21: 'instantiate var=iv with='v_x_0' occ=2' 
819520     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 22: 'rule impLeft' 
819521     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 23: 'tryclose branch' 
819748     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 24: 'rule exLeft' 
819752     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 25: 'rule andLeft' 
819753     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 26: 'rule andLeft' 
819754     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 27: 'instantiate hide var=iv with='v_y_0' occ=2' 
819756     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 28: 'rule impLeft' 
819761     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 29: 'tryclose branch' 
819924     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 30: 'rule exLeft' 
819926     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 31: 'rule andLeft' 
819928     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 32: 'rule andLeft' 
819929     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 33: 'instantiate var=iv with='jv_0' occ=1' 
819930     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 34: 'rule impLeft' 
819931     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 35: 'tryclose branch' 
819942     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 36: 'rule andLeft' 
819943     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 37: 'rule andLeft' 
819944     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 38: 'rule castAdd formula='s_0[jv_0] = v_x_0' occ=0' 
819947     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 39: 'instantiate hide var=iv with='jv_1' occ=1' 
819950     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 40: 'rule impLeft' 
819952     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 41: 'tryclose branch' 
819963     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 42: 'rule andLeft' 
819964     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 43: 'rule andLeft' 
819966     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 44: 'rule castAdd formula='s_0[jv_1] = v_y_0' occ=0' 
819967     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 45: 'instantiate var=iv  with='v_x_0'' 
819968     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 46: 'rule impLeft' 
819969     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 47: 'tryclose branch' 
820134     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 48: 'instantiate var=iv  with='v_y_0'' 
820136     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 49: 'rule impLeft' 
820138     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 50: 'tryclose branch' 
820295     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 51: 'cut 'v_x_0 = v_y_0'' 
820298     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 52: 'instantiate hide var='v_r' with='seqSwap(s_0,v_x_0,jv_0)'' 
820301     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 53: 'rule andRight' 
820302     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 54: 'rule andRight' 
820304     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 55: 'rule andRight' 
820306     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 56: 'rule andRight' 
820307     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 57: 'rule lenOfSwap' 
820309     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 58: 'tryclose branch' 
820314     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 59: 'rule seqNPermSwapNPerm' 
820316     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 60: 'instantiate hide var='iv' with='v_x_0' occ=1' 
820317     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 61: 'instantiate hide var='jv' with='jv_0'' 
820318     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 62: 'rule impLeft' 
820319     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 63: 'tryclose branch' 
820460     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 64: 'tryclose branch' 
820465     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 65: 'rule allRight' 
820467     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 66: 'rule impRight' 
820468     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 67: 'rule andLeft' 
820469     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 68: 'instantiate var=iv with='v_iv_0'' 
820470     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 69: 'rule impLeft' 
820472     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 70: 'tryclose branch' 
820626     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 71: 'rule getOfSwap' 
820628     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 72: 'rule ifthenelse_negated' 
820630     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 73: 'rule ifthenelse_split occ=0' 
820632     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 74: 'rule andLeft' 
820633     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 75: 'rule andLeft' 
820634     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 76: 'rule andLeft' 
820634     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 77: 'rule ifthenelse_split occ=0' 
820636     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 78: 'tryclose branch' 
820760     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 79: 'rule ifthenelse_split occ=0' 
820762     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 80: 'tryclose branch' 
820893     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 81: 'tryclose branch' 
820898     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 82: 'tryclose branch' 
820903     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 83: 'rule getOfSwap' 
820905     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 84: 'rule ifthenelse_negated' 
820906     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 85: 'rule ifthenelse_split occ=0' 
820908     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 86: 'rule andLeft' 
820908     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 87: 'rule andLeft' 
820909     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 88: 'rule andLeft' 
820910     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 89: 'rule ifthenelse_split occ=0' 
820911     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 90: 'tryclose branch' 
820922     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 91: 'tryclose branch' 
820928     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 92: 'tryclose branch' 
821057     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 93: 'rule getOfSwap' 
821059     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 94: 'rule ifthenelse_negated' 
821060     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 95: 'rule ifthenelse_split occ=0' 
821061     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 96: 'rule andLeft' 
821062     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 97: 'rule andLeft' 
821063     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 98: 'rule andLeft' 
821063     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 99: 'rule ifthenelse_split occ=0' 
821065     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 100: 'tryclose branch' 
821133     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 101: 'tryclose branch' 
821140     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 102: 'tryclose branch' 
821267     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 103: 'cut '(int)s_0[v_x_0] = (int)s_0[v_y_0]'' 
821269     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 104: 'rule seqNPermInjective' 
821271     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 105: 'instantiate hide var=iv with='v_x_0'' 
821273     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 106: 'instantiate hide var=jv with='v_y_0'' 
821274     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 107: 'rule impLeft' 
821275     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 108: 'tryclose branch' 
821433     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 109: 'tryclose branch' 
821437     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 110: 'cut '(int)s_0[v_x_0] = v_x_0'' 
821439     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 111: 'instantiate hide var=v_r with='seqSwap(s_0,v_y_0,jv_1)'' 
821441     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 112: 'rule andRight' 
821443     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 113: 'rule andRight' 
821444     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 114: 'rule andRight' 
821445     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 115: 'rule andRight' 
821446     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 116: 'tryclose branch' 
821457     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 117: 'rule seqNPermSwapNPerm' 
821459     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 118: 'instantiate hide var=iv with='v_y_0'' 
821467     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 119: 'instantiate hide var=jv with='jv_1'' 
821468     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 120: 'tryclose branch' 
821643     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 121: 'rule allRight' 
821645     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 122: 'rule impRight' 
821647     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 123: 'rule andLeft' 
821647     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 124: 'instantiate var=iv with='v_iv_0'' 
821648     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 125: 'rule impLeft' 
821649     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 126: 'tryclose branch' 
821780     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 127: 'rule getOfSwap' 
821782     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 128: 'rule ifthenelse_negated' 
821783     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 129: 'rule ifthenelse_split occ=0' 
821784     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 130: 'rule andLeft' 
821785     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 131: 'rule andLeft' 
821786     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 132: 'rule andLeft' 
821787     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 133: 'rule ifthenelse_split occ=0' 
821789     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 134: 'tryclose branch' 
821892     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 135: 'rule ifthenelse_split occ=0' 
821894     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 136: 'tryclose branch' 
821986     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 137: 'instantiate var=iv with='v_y_0'' 
821987     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 138: 'rule impLeft' 
821988     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 139: 'tryclose branch' 
821993     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 140: 'tryclose branch' 
821997     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 141: 'tryclose branch' 
822003     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 142: 'tryclose branch' 
822154     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 143: 'rule getOfSwap' 
822156     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 144: 'rule ifthenelse_negated' 
822158     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 145: 'rule ifthenelse_split occ=0' 
822160     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 146: 'tryclose branch' 
822176     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 147: 'tryclose branch' 
822294     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 148: 'tryclose branch' 
826856     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 149: 'cut  '(int)s_0[v_y_0] = v_y_0'' 
826857     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 150: 'instantiate hide var=v_r with='seqSwap(s_0,v_x_0,jv_0)'' 
826865     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 151: 'rule andRight' 
826867     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 152: 'rule andRight' 
826868     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 153: 'rule andRight' 
826868     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 154: 'rule andRight' 
826869     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 155: 'tryclose branch' 
826880     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 156: 'rule seqNPermSwapNPerm' 
826883     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 157: 'instantiate hide var=iv with='v_x_0'' 
826885     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 158: 'instantiate hide var=jv with='jv_0'' 
826886     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 159: 'rule impLeft' 
826887     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 160: 'tryclose branch' 
827018     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 161: 'tryclose branch' 
827023     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 162: 'rule allRight' 
827025     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 163: 'rule impRight' 
827026     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 164: 'rule andLeft' 
827026     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 165: 'instantiate var=iv with='v_iv_0'' 
827027     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 166: 'rule impLeft' 
827028     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 167: 'tryclose branch' 
827170     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 168: 'rule getOfSwap' 
827173     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 169: 'rule ifthenelse_negated' 
827174     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 170: 'rule ifthenelse_split occ=0' 
827175     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 171: 'rule andLeft' 
827176     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 172: 'rule andLeft' 
827177     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 173: 'rule andLeft' 
827178     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 174: 'rule ifthenelse_split occ=0' 
827179     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 175: 'tryclose branch' 
827290     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 176: 'rule ifthenelse_split occ=0' 
827292     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 177: 'tryclose branch' 
827462     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 178: 'tryclose branch' 
827468     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 179: 'tryclose branch' 
827474     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 180: 'rule getOfSwap' 
827475     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 181: 'rule ifthenelse_negated' 
827476     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 182: 'rule ifthenelse_split occ=0' 
827477     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 183: 'tryclose branch' 
827493     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 184: 'tryclose branch' 
827601     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 185: 'rule getOfSwap' 
827602     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 186: 'rule ifthenelse_negated' 
827603     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 187: 'rule ifthenelse_split occ=0' 
827605     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 188: 'tryclose branch' 
827714     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 189: 'tryclose branch' 
827727     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 190: 'cut '(int)s_0[v_x_0]=v_y_0'' 
827728     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 191: 'instantiate hide var=v_r with='seqSwap(seqSwap(s_0,jv_0,v_x_0),jv_0,v_y_0)'' 
827730     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 192: 'rule andRight' 
827731     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 193: 'rule andRight' 
827732     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 194: 'rule andRight' 
827733     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 195: 'rule andRight' 
827734     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 196: 'tryclose branch' 
827747     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 197: 'rule seqNPermSwapNPerm' 
827749     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 198: 'instantiate hide var=iv with='jv_0'' 
827750     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 199: 'instantiate hide var=jv with='v_x_0'' 
827751     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 200: 'rule impLeft' 
827752     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 201: 'tryclose branch' 
827873     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 202: 'rule seqNPermSwapNPerm formula='seqNPerm(seqSwap(s_0, jv_0, v_x_0))'' 
827875     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 203: 'instantiate hide var=iv with='jv_0'' 
827877     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 204: 'instantiate hide var=jv with='v_y_0'' 
827878     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 205: 'rule impLeft' 
827878     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 206: 'tryclose branch' 
827998     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 207: 'tryclose branch' 
828004     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 208: 'rule allRight' 
828005     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 209: 'rule impRight' 
828006     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 210: 'rule andLeft' 
828006     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 211: 'instantiate var=iv with='v_iv_0'' 
828007     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 212: 'rule impLeft' 
828008     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 213: 'tryclose branch' 
828141     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 214: 'rule getOfSwap' 
828143     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 215: 'rule ifthenelse_negated' 
828144     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 216: 'rule ifthenelse_split occ=0' 
828145     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 217: 'rule andLeft' 
828146     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 218: 'rule andLeft' 
828147     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 219: 'rule andLeft' 
828148     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 220: 'rule ifthenelse_split occ=0' 
828149     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 221: 'rule getOfSwap' 
828150     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 222: 'rule ifthenelse_negated' 
828151     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 223: 'rule ifthenelse_split occ=0' 
828153     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 224: 'rule andLeft' 
828153     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 225: 'rule andLeft' 
828155     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 226: 'rule andLeft' 
828155     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 227: 'rule ifthenelse_split occ=0' 
828157     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 228: 'tryclose branch' 
828271     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 229: 'rule ifthenelse_split occ=0' 
828273     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 230: 'tryclose branch' 
828280     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 231: 'tryclose branch' 
828383     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 232: 'tryclose branch' 
828502     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 233: 'rule ifthenelse_split' 
828504     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 234: 'rule getOfSwap' 
828505     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 235: 'rule ifthenelse_negated' 
828506     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 236: 'rule ifthenelse_split occ=0' 
828507     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 237: 'rule andLeft' 
828507     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 238: 'rule andLeft' 
828508     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 239: 'rule andLeft' 
828508     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 240: 'rule ifthenelse_split occ=0' 
828510     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 241: 'tryclose branch' 
828628     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 242: 'tryclose branch' 
828636     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 243: 'tryclose branch' 
828757     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 244: 'rule getOfSwap' 
828758     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 245: 'rule ifthenelse_negated' 
828759     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 246: 'rule ifthenelse_split occ=0' 
828762     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 247: 'rule andLeft' 
828763     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 248: 'rule andLeft' 
828763     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 249: 'rule andLeft' 
828764     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 250: 'rule ifthenelse_split occ=0' 
828765     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 251: 'tryclose branch' 
828773     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 252: 'rule ifthenelse_split occ=0' 
828774     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 253: 'tryclose branch' 
828881     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 254: 'tryclose branch' 
828890     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 255: 'tryclose branch' 
828898     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 256: 'tryclose branch' 
829034     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 257: 'rule getOfSwap' 
829036     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 258: 'rule ifthenelse_negated' 
829037     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 259: 'rule ifthenelse_split occ=0' 
829038     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 260: 'rule andLeft' 
829038     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 261: 'rule andLeft' 
829039     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 262: 'rule andLeft' 
829039     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 263: 'rule ifthenelse_split occ=0' 
829040     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 264: 'tryclose branch' 
829114     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 265: 'rule ifthenelse_split occ=0' 
829115     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 266: 'rule getOfSwap' 
829116     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 267: 'rule ifthenelse_negated' 
829116     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 268: 'rule ifthenelse_split occ=0' 
829117     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 269: 'tryclose branch' 
829125     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 270: 'tryclose branch' 
829131     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 271: 'tryclose branch' 
829292     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 272: 'tryclose branch' 
829417     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 273: 'rule getOfSwap' 
829419     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 274: 'rule ifthenelse_negated' 
829420     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 275: 'rule ifthenelse_split occ=0' 
829421     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 276: 'tryclose branch' 
829661     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 277: 'tryclose branch' 
829782     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 278: 'cut 'int::seqGet(s_0, v_y_0)=v_x_0'' 
829783     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 279: 'tryclose branch' 
833814     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 280: 'rule seqNPermSwapNPerm' 
833828     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 281: 'instantiate hide var=iv with='jv_1'' 
833830     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 282: 'instantiate hide var=jv with='v_y_0'' 
833831     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 283: 'rule impLeft' 
833835     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 284: 'tryclose branch' 
834003     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 285: 'rule seqNPermSwapNPerm formula='seqNPerm(seqSwap(s_0,jv_1,v_y_0))'' 
834005     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 286: 'instantiate hide var=iv with='jv_1'' 
834006     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 287: 'instantiate hide var=jv with='v_x_0'' 
834008     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 288: 'rule impLeft' 
834009     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 289: 'tryclose branch' 
834149     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 290: 'tryclose branch' 
838058     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 291: 'tryclose branch' 
842081     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 292: 'rule seqNPermSwapNPerm formula='seqNPerm(s_0)'' 
842087     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 293: 'instantiate hide var=iv with='v_x_0'' 
842088     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 294: 'instantiate hide var=jv with='jv_0'' 
842088     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 295: 'rule impLeft' 
842089     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 296: 'tryclose branch' 
842240     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 297: 'rule seqNPermSwapNPerm formula='seqNPerm(seqSwap(s_0,v_x_0,jv_0))'' 
842242     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 298: 'instantiate hide var=iv with='v_y_0'' 
842243     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 299: 'instantiate hide var=jv with='jv_1'' 
842244     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 300: 'instantiate hide var=v_r with='seqSwap(seqSwap(s_0, v_x_0, jv_0), v_y_0, jv_1)' ...' 
842246     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 301: 'tryclose branch' 
843777     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm2/Taclet_schiffl_thm_1.proof 
843777     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 98.6ns 
843778     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
846899     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.12s 
846900     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: schiffl_thm_1 
847953     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: schiffl_thm_1 
847955     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 8.5ns 
847956     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 1: 'macro split-prop' 
847967     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 2: 'rule schiffl_lemma_2 formula='seqPerm(f_s, f_t)'' 
847980     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 3: 'instantiate hide var=x with='f_x'' 
847983     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 4: 'instantiate hide var=y with='f_y'' 
847985     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 5: 'rule impLeft' 
847985     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 6: 'tryclose branch' 
847991     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 7: 'rule exLeft' 
847993     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 8: 'macro split-prop' 
847998     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 9: 'rule seqPermDef occ=1' 
848001     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 10: 'rule andRight' 
848002     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 11: 'tryclose branch' 
848015     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 12: 'instantiate hide var=s with='r_0'' 
848017     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 13: 'rule andRight' 
848018     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 14: 'tryclose branch' 
848086     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 15: 'rule allRight' 
848087     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 16: 'rule impRight' 
848088     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 17: 'instantiate hide var=iv with='iv_0'' 
848089     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 18: 'rule impLeft' 
848089     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 19: 'tryclose branch' 
848176     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 20: 'rule andLeft' 
848176     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 21: 'rule seqNPermRange' 
848179     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 22: 'instantiate hide var=iv with='iv_0'' 
848180     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 23: 'rule impLeft' 
848181     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 24: 'tryclose branch' 
848186     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 25: 'rule andLeft' 
848186     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 26: 'rule andLeft' 
848187     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 27: 'rule seqNPermRange' 
848189     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 28: 'instantiate hide var=iv with='f_x'' 
848189     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 29: 'rule impLeft' 
848190     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 30: 'tryclose branch' 
848302     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 31: 'rule andLeft' 
848303     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 32: 'rule andLeft' 
848304     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 33: 'rule seqNPermRange' 
848306     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 34: 'instantiate hide var=iv with='f_y'' 
848307     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 35: 'rule impLeft' 
848307     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 36: 'tryclose branch' 
848435     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 37: 'rule andLeft' 
848436     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 38: 'rule andLeft' 
848437     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 39: 'rule getOfSeqDef occ=0' 
848437     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 40: 'rule getOfSeqDef' 
848438     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 41: 'rule ifthenelse_split occ=0' 
848440     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 42: 'rule andLeft occ=0' 
848440     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 43: 'rule sub_zero_2 occ=0' 
848441     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 44: 'rule ifthenelse_split occ=2' 
848442     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 45: 'rule andLeft' 
848442     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 46: 'rule sub_zero_2 occ=0' 
848443     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 47: 'rule add_zero_right occ=0' 
848443     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 48: 'rule add_zero_right occ=0' 
848444     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 49: 'rule add_zero_right occ=0' 
848444     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 50: 'rule add_zero_right occ=0' 
848445     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 51: 'rule add_zero_right occ=0' 
848446     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 52: 'rule add_zero_right occ=0' 
848447     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 53: 'rule ifthenelse_split occ=0' 
848448     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 54: 'rule ifthenelse_split occ=0' 
848449     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 55: 'tryclose branch' 
848452     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 56: 'tryclose branch' 
848508     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 57: 'rule ifthenelse_split occ=0' 
848509     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 58: 'tryclose branch' 
848593     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 59: 'rule ifthenelse_split occ=0' 
848594     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 60: 'rule seqNPermInjective' 
848596     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 61: 'instantiate hide var=iv with='iv_0'' 
848598     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 62: 'instantiate hide var=jv with='f_y'' 
848599     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 63: 'rule impLeft' 
848599     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 64: 'tryclose branch' 
848669     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 65: 'tryclose branch' 
848672     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 66: 'rule ifthenelse_split occ=0' 
848673     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 67: 'rule seqNPermInjective' 
848675     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 68: 'instantiate hide var=iv with='iv_0'' 
848677     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 69: 'instantiate hide var=jv with='f_x'' 
848677     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 70: 'rule impLeft' 
848678     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 71: 'tryclose branch' 
848748     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 72: 'tryclose branch' 
848752     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 73: 'tryclose branch' 
848756     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 74: 'tryclose branch' 
848934     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 75: 'tryclose branch' 
849014     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_eqSameSeq.proof 
849016     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 2.64ms 
849018     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
852094     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.08s 
852094     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: eqSameSeq 
853198     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: eqSameSeq 
853252     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 50.59ms