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

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

tests
0

failures
0

ignored
14m0.44s

duration
100%

successful

Tests

Test Method name Duration Result
powPositive data()[100] 4.006s passed
powPositiveConcrete data()[101] 4.039s passed
powGeq1Concrete data()[102] 3.987s passed
pow2InIntLower data()[103] 3.977s passed
pow2InIntUpper data()[104] 4.025s passed
logSelfConcrete data()[105] 4.062s passed
log1Concrete data()[106] 4.079s passed
logProduct data()[107] 4.014s passed
logTimesBaseConcrete data()[108] 3.967s passed
logProdIdentity data()[109] 4.129s passed
moduloByteIsInByte data()[10] 4.158s passed
logProdIdentityConcrete data()[110] 4.021s passed
logPowIdentity data()[111] 4.023s passed
logPowIdentityConcrete data()[112] 4.056s passed
logPositive data()[113] 4.090s passed
logPositiveConcrete data()[114] 4.072s passed
logMono data()[115] 4.108s passed
logMonoConcrete data()[116] 4.021s passed
powLogLess data()[117] 4.032s passed
powLogMore2 data()[118] 4.077s passed
logLessThanPow data()[119] 4.037s passed
moduloCharIsInChar data()[11] 4.183s passed
logLessThanPowConcrete data()[120] 4.036s passed
logSqueeze data()[121] 4.060s passed
ifthenelse_equals data()[122] 4.128s passed
ifthenelse_equals_1 data()[123] 4.135s passed
ifthenelse_equals_2 data()[124] 4.076s passed
disjointWithSingleton1 data()[125] 4.070s passed
disjointWithSingleton2 data()[126] 4.100s passed
disjointArrayRanges data()[127] 4.074s passed
disjointArrayRangeAllFields1 data()[128] 4.058s passed
disjointArrayRangeAllFields2 data()[129] 4.075s passed
div_unique1 data()[12] 4.349s passed
seqSelfDefinition data()[130] 4.093s passed
seqOutsideValue data()[131] 4.082s passed
castedGetAny data()[132] 4.105s passed
seqGetAlphaCast data()[133] 4.045s passed
getOfSeqSingleton data()[134] 4.096s passed
getOfSeqSingletonConcrete data()[135] 4.028s passed
getOfSeqConcat data()[136] 4.057s passed
getOfSeqSub data()[137] 4.097s passed
getOfSeqReverse data()[138] 4.065s passed
lenOfSeqEmpty data()[139] 4.087s passed
div_unique2 data()[13] 4.209s passed
lenOfSeqSingleton data()[140] 4.091s passed
lenOfSeqConcat data()[141] 4.107s passed
lenOfSeqSub data()[142] 4.053s passed
lenOfSeqReverse data()[143] 4.047s passed
equalityToSeqGetAndSeqLenLeft data()[144] 4.076s passed
equalityToSeqGetAndSeqLenRight data()[145] 4.088s passed
getOfSeqSingletonEQ data()[146] 4.074s passed
getOfSeqConcatEQ data()[147] 4.087s passed
getOfSeqSubEQ data()[148] 3.996s passed
getOfSeqReverseEQ data()[149] 4.102s passed
div_exists data()[14] 4.449s passed
lenOfSeqEmptyEQ data()[150] 4.093s passed
lenOfSeqSingletonEQ data()[151] 4.069s passed
lenOfSeqConcatEQ data()[152] 4.046s passed
lenOfSeqSubEQ data()[153] 4.049s passed
lenOfSeqReverseEQ data()[154] 4.135s passed
getOfSeqDefEQ data()[155] 4.107s passed
lenOfSeqDefEQ data()[156] 4.122s passed
seqConcatWithSeqEmpty1 data()[157] 4.110s passed
seqConcatWithSeqEmpty2 data()[158] 4.151s passed
seqReverseOfSeqEmpty data()[159] 4.090s passed
div_one data()[15] 4.192s passed
subSeqComplete data()[160] 4.073s passed
subSeqTailR data()[161] 4.082s passed
subSeqTailL data()[162] 4.102s passed
subSeqTailEQR data()[163] 4.111s passed
subSeqTailEQL data()[164] 4.082s passed
seqDef_split data()[165] 4.144s passed
seqDef_induction_upper data()[166] 4.185s passed
seqDef_induction_upper_concrete data()[167] 4.112s passed
seqDef_induction_lower data()[168] 4.161s passed
seqDef_induction_lower_concrete data()[169] 4.229s passed
jdiv_one data()[16] 4.139s passed
seqDef_split_in_three data()[170] 4.324s passed
seqDef_empty data()[171] 4.152s passed
seqDef_one_summand data()[172] 4.137s passed
seqDef_lower_equals_upper data()[173] 4.057s passed
seqDefOfSeq data()[174] 4.173s passed
seqSelfDefinitionEQ2 data()[175] 4.139s passed
indexOfSeqSingleton data()[176] 4.059s passed
indexOfSeqConcatFirst data()[177] 4.067s passed
indexOfSeqConcatSecond data()[178] 4.186s passed
indexOfSeqSub data()[179] 4.109s passed
div_zero data()[17] 4.128s passed
lenOfArray2seq data()[180] 4.101s passed
getAnyOfArray2seq data()[181] 4.110s passed
getOfArray2seq data()[182] 4.113s passed
getAnyOfNPermInv data()[183] 4.139s passed
seqNPermRange data()[184] 4.155s passed
seqPermTrans data()[185] 4.143s passed
seqPermRefl data()[186] 4.101s passed
seqPermSplit data()[187] 4.039s passed
seqNPermRight data()[188] 4.391s passed
seqPermFromSwap data()[189] 4.169s passed
divResZero1 data()[18] 4.129s passed
seqPermTransAlt0 data()[190] 4.022s passed
seqPermTransAlt1 data()[191] 4.037s passed
seqPermTransAlt2 data()[192] 4.068s passed
seqPermTransAlt3 data()[193] 4.134s passed
seqPermForall data()[194] 4.242s passed
seqPermExists data()[195] 4.162s passed
schiffl_lemma_2 data()[196] 27.849s passed
schiffl_thm_1 data()[197] 5.078s passed
eqSameSeq data()[198] 4.322s passed
divResZero2 data()[19] 4.113s passed
eqTermCut data()[1] 4.891s passed
divResOne1 data()[20] 4.124s passed
divResOne2 data()[21] 4.279s passed
div_cancel1 data()[22] 4.209s passed
div_cancel2 data()[23] 4.172s passed
divAddMultDenom data()[24] 4.179s passed
divMinus data()[25] 4.376s passed
divMinusDenom data()[26] 4.153s passed
divLeastDPos data()[27] 4.131s passed
divLeastDNeg data()[28] 4.175s passed
divGreatestDPos data()[29] 4.105s passed
equivAllRight data()[2] 4.539s passed
divGreatestDNeg data()[30] 4.065s passed
divIncreasingPos data()[31] 4.030s passed
divIncreasingNeg data()[32] 4.167s passed
jdiv_zero data()[33] 4.122s passed
jdivPulloutMinusNum data()[34] 4.148s passed
jdivPulloutMinusDenom data()[35] 4.213s passed
jdiv_uniquePosPos data()[36] 4.122s passed
jdiv_uniquePosNeg data()[37] 4.183s passed
jdiv_uniqueNegPos data()[38] 4.115s passed
jdiv_uniqueNegNeg data()[39] 4.112s passed
irrflConcrete1 data()[3] 4.460s passed
jdivMultDenom1 data()[40] 4.201s passed
jdivMultDenom2 data()[41] 4.136s passed
mod_geZero data()[42] 4.089s passed
mod_lessDenom data()[43] 4.031s passed
jmod_NumPos data()[44] 4.130s passed
jmod_NumNeg data()[45] 4.187s passed
jmod_geZero data()[46] 4.134s passed
jmodNumZero data()[47] 4.180s passed
jmod_pulloutminusNum data()[48] 4.150s passed
jmod_pulloutminusDenom data()[49] 4.174s passed
irrflConcrete2 data()[4] 4.325s passed
jmodUnique1 data()[50] 4.222s passed
jmodUnique2 data()[51] 4.231s passed
intDivRem data()[52] 4.066s passed
jmodjmod data()[53] 4.187s passed
jmodDivisible data()[54] 4.057s passed
jmodDivisibleRep data()[55] 4.057s passed
jdivAddMultDenom data()[56] 4.252s passed
jmodAltZero data()[57] 4.168s passed
jmodAddMultDenomZero data()[58] 4.112s passed
polyDiv_zero data()[59] 4.010s passed
cancel_gtPos data()[5] 4.299s passed
polyMod_ltdivDenom data()[60] 4.099s passed
bsum_empty data()[61] 3.984s passed
bsum_induction_upper data()[62] 4.008s passed
bsum_induction_lower data()[63] 3.991s passed
bsum_num_of_bounds data()[64] 4.070s passed
bsum_num_of_bounds2 data()[65] 4.062s passed
bsum_induction_upper2 data()[66] 4.108s passed
bsum_induction_upper_concrete data()[67] 4.106s passed
bsum_induction_upper_concrete_2 data()[68] 4.060s passed
bsum_induction_upper2_concrete data()[69] 4.053s passed
cancel_gtNeg data()[6] 4.249s passed
bsum_induction_lower_concrete data()[70] 4.037s passed
bsum_induction_lower2 data()[71] 4.041s passed
bsum_induction_lower2_concrete data()[72] 4.041s passed
bsum_positive data()[73] 4.107s passed
bsum_upper_bound data()[74] 4.048s passed
bsum_lower_bound data()[75] 4.140s passed
bsum_positive_lower_bound_element data()[76] 4.107s passed
bsum_sub_same_index data()[77] 4.112s passed
bsum_less_same_index data()[78] 4.099s passed
bsum_equal_except_one_index data()[79] 4.088s passed
moduloIntIsInInt data()[7] 4.224s passed
bsum_num_of_is_max data()[80] 4.040s passed
bsum_num_of_is_max2 data()[81] 4.161s passed
bsum_num_of_is_max3 data()[82] 4.043s passed
bsum_num_of_is_max4 data()[83] 4.105s passed
bsum_num_of_lt_max data()[84] 4.047s passed
bsum_num_of_lt_max2 data()[85] 4.116s passed
bsum_num_of_lt_max3 data()[86] 4.057s passed
bsum_num_of_lt_max4 data()[87] 4.071s passed
bsum_num_of_gt0 data()[88] 4.132s passed
bsum_num_of_gt0_alt data()[89] 4.044s passed
moduloLongIsInLong data()[8] 4.306s passed
bsum_add_concrete data()[90] 4.089s passed
bprod_all_positive data()[91] 4.036s passed
bprod_split data()[92] 4.053s passed
powConcrete0 data()[93] 4.029s passed
powConcrete1 data()[94] 4.086s passed
powSplitFactor data()[95] 4.087s passed
powAdd data()[96] 4.058s passed
powMono data()[97] 4.131s passed
powMonoConcrete data()[98] 4.039s passed
powMonoConcreteRight data()[99] 4.051s passed
moduloShortIsInShort data()[9] 4.171s passed

Standard output

381        INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src/test/resources/testcase/dummyTrue.key 
411        DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 8.87ms 
726        INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
750        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)

1948       DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for Meta 
1951       DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for Meta 
1954       DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for Meta 
1955       DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for Meta 
3880       DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for JavaBigintExpression 
10439      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 9.71s 
10551      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof dummyTrue.key 
10599      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 38.6ns 
10617      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/firstOrder/Taclet_eqTermCut.proof 
10619      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 1.8ms 
10627      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
14260      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.63s 
14264      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: eqTermCut 
15458      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: eqTermCut 
15495      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 25.95ms 
15510      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/firstOrder/Taclet_equivAllRight.proof 
15510      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 236.8ns 
15513      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
18909      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.4s 
18910      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: equivAllRight 
20023      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: equivAllRight 
20045      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 17.74ms 
20050      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_irrflConcrete1.proof 
20051      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 405.3ns 
20054      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
23411      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.36s 
23412      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: irrflConcrete1 
24485      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: irrflConcrete1 
24505      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 13.12ms 
24510      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_irrflConcrete2.proof 
24510      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 157.4ns 
24515      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
27777      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.26s 
27777      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: irrflConcrete2 
28826      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: irrflConcrete2 
28833      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.53ms 
28837      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_cancel_gtPos.proof 
28838      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 1.01ms 
28840      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
32028      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.19s 
32029      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: cancel_gtPos 
33067      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: cancel_gtPos 
33133      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 62.22ms 
33137      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_cancel_gtNeg.proof 
33138      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 567.11ns 
33140      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
36299      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.16s 
36299      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: cancel_gtNeg 
37332      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: cancel_gtNeg 
37382      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 44.44ms 
37388      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intRulesIgnoringOF/Taclet_moduloIntIsInInt.proof 
37389      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 440.31ns 
37390      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
40581      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.19s 
40582      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: moduloIntIsInInt 
41561      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: moduloIntIsInInt 
41607      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.05ms 
41614      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intRulesIgnoringOF/Taclet_moduloLongIsInLong.proof 
41615      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 837.31ns 
41618      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
44885      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.27s 
44885      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: moduloLongIsInLong 
45907      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: moduloLongIsInLong 
45915      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 722.01ns 
45921      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intRulesIgnoringOF/Taclet_moduloShortIsInShort.proof 
45922      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 394.61ns 
45923      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
49081      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.16s 
49082      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: moduloShortIsInShort 
50088      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: moduloShortIsInShort 
50091      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 707.41ns 
50094      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intRulesIgnoringOF/Taclet_moduloByteIsInByte.proof 
50094      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 377.31ns 
50096      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
53240      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.14s 
53240      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: moduloByteIsInByte 
54245      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: moduloByteIsInByte 
54249      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 683.71ns 
54252      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intRulesIgnoringOF/Taclet_moduloCharIsInChar.proof 
54252      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 373.11ns 
54253      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
57407      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.15s 
57408      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: moduloCharIsInChar 
58429      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: moduloCharIsInChar 
58432      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 600ns 
58435      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_div_unique1.proof 
58436      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 416.9ns 
58437      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
61604      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.17s 
61604      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: div_unique1 
62700      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: div_unique1 
62777      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 71.02ms 
62790      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_div_unique2.proof 
62791      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 780.41ns 
62793      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
65925      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.13s 
65925      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: div_unique2 
66945      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: div_unique2 
66993      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 43.69ms 
66996      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_div_exists.proof 
66997      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 395.3ns 
66999      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
70157      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.16s 
70158      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: div_exists 
71168      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: div_exists 
71442      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 262.74ms 
71447      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_div_one.proof 
71447      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 448.11ns 
71449      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
74563      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.11s 
74564      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: div_one 
75630      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: div_one 
75636      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.88ms 
75638      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdiv_one.proof 
75640      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 1.65ms 
75641      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
78762      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.12s 
78764      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdiv_one 
79771      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdiv_one 
79775      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.54ms 
79779      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_div_zero.proof 
79779      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 346.9ns 
79781      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
82822      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.04s 
82823      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: div_zero 
83843      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: div_zero 
83904      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 54.87ms 
83908      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divResZero1.proof 
83908      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 367.1ns 
83909      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
87016      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.11s 
87017      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divResZero1 
88010      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divResZero1 
88034      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 19.44ms 
88037      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divResZero2.proof 
88037      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 365ns 
88038      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
91113      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.07s 
91114      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divResZero2 
92126      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divResZero2 
92147      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 17.58ms 
92150      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divResOne1.proof 
92150      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 371.3ns 
92152      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
95264      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.11s 
95265      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divResOne1 
96245      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divResOne1 
96271      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 22.86ms 
96273      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divResOne2.proof 
96273      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 223.5ns 
96275      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
99441      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.17s 
99442      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divResOne2 
100528     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divResOne2 
100550     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 18.04ms 
100552     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_div_cancel1.proof 
100553     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 268.8ns 
100554     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
103727     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.17s 
103728     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: div_cancel1 
104706     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: div_cancel1 
104759     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 41.2ms 
104762     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_div_cancel2.proof 
104762     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 383.51ns 
104764     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
107924     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.16s 
107924     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: div_cancel2 
108926     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: div_cancel2 
108931     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.47ms 
108933     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divAddMultDenom.proof 
108934     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 367.81ns 
108935     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
112018     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.08s 
112020     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divAddMultDenom 
113037     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divAddMultDenom 
113100     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 55.73ms 
113113     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divMinus.proof 
113113     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 405.81ns 
113114     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
116352     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.24s 
116353     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divMinus 
117397     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divMinus 
117486     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 80.64ms 
117490     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divMinusDenom.proof 
117490     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 388.8ns 
117492     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
120563     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.07s 
120563     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divMinusDenom 
121567     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divMinusDenom 
121639     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 65.01ms 
121644     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divLeastDPos.proof 
121646     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 1.76ms 
121649     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
124741     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.09s 
124743     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divLeastDPos 
125753     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divLeastDPos 
125772     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 15.51ms 
125774     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divLeastDNeg.proof 
125774     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 145.1ns 
125775     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
128920     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.15s 
128921     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divLeastDNeg 
129926     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divLeastDNeg 
129946     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 16.64ms 
129949     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divGreatestDPos.proof 
129949     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 203.2ns 
129950     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
133015     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.06s 
133015     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divGreatestDPos 
134028     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divGreatestDPos 
134051     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 15.46ms 
134054     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divGreatestDNeg.proof 
134055     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 377.1ns 
134056     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
137127     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.07s 
137127     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divGreatestDNeg 
138107     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divGreatestDNeg 
138118     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 8.09ms 
138119     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divIncreasingPos.proof 
138119     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 91.2ns 
138120     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
141169     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.05s 
141169     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divIncreasingPos 
142138     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divIncreasingPos 
142147     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 7.38ms 
142149     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divIncreasingNeg.proof 
142149     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 97.8ns 
142150     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
145271     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.12s 
145271     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divIncreasingNeg 
146302     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divIncreasingNeg 
146314     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 8.75ms 
146316     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdiv_zero.proof 
146316     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 143.3ns 
146317     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
149473     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.16s 
149473     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdiv_zero 
150428     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdiv_zero 
150436     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.57ms 
150440     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdivPulloutMinusNum.proof 
150440     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 118.3ns 
150441     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
153549     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.11s 
153550     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdivPulloutMinusNum 
154567     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdivPulloutMinusNum 
154586     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 15.88ms 
154587     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdivPulloutMinusDenom.proof 
154588     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 105.9ns 
154589     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
157726     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.14s 
157728     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdivPulloutMinusDenom 
158705     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdivPulloutMinusDenom 
158798     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 85.49ms 
158803     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdiv_uniquePosPos.proof 
158803     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 335.6ns 
158805     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
161904     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.1s 
161905     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdiv_uniquePosPos 
162892     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdiv_uniquePosPos 
162921     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 24.63ms 
162924     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdiv_uniquePosNeg.proof 
162924     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 321.7ns 
162926     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
166078     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.15s 
166078     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdiv_uniquePosNeg 
167076     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdiv_uniquePosNeg 
167105     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 25.16ms 
167106     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdiv_uniqueNegPos.proof 
167107     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 115.2ns 
167108     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
170193     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.09s 
170193     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdiv_uniqueNegPos 
171192     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdiv_uniqueNegPos 
171220     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 25.03ms 
171222     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdiv_uniqueNegNeg.proof 
171223     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 193.7ns 
171224     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
174295     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.07s 
174295     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdiv_uniqueNegNeg 
175299     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdiv_uniqueNegNeg 
175332     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 28.36ms 
175334     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdivMultDenom1.proof 
175334     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 109.7ns 
175335     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
178459     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.12s 
178459     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdivMultDenom1 
179456     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdivMultDenom1 
179530     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 63.97ms 
179538     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdivMultDenom2.proof 
179538     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 132.2ns 
179540     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
182631     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.09s 
182632     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdivMultDenom2 
183665     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdivMultDenom2 
183672     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.71ms 
183676     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_mod_geZero.proof 
183676     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 112.9ns 
183677     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
186763     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.09s 
186764     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: mod_geZero 
187755     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: mod_geZero 
187761     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.23ms 
187763     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_mod_lessDenom.proof 
187763     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 103.2ns 
187764     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
190798     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.03s 
190799     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: mod_lessDenom 
191780     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: mod_lessDenom 
191792     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 8.9ms 
191793     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmod_NumPos.proof 
191793     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 87.5ns 
191794     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
194925     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.13s 
194925     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmod_NumPos 
195909     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmod_NumPos 
195922     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 9.21ms 
195924     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmod_NumNeg.proof 
195925     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 327.3ns 
195926     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
199068     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.14s 
199069     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmod_NumNeg 
200080     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmod_NumNeg 
200109     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 25.51ms 
200111     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmod_geZero.proof 
200111     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 124.2ns 
200112     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
203229     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.12s 
203229     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmod_geZero 
204230     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmod_geZero 
204243     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 9.94ms 
204244     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmodNumZero.proof 
204245     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 144ns 
204245     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
207388     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.14s 
207388     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmodNumZero 
208418     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmodNumZero 
208423     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.02ms 
208425     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmod_pulloutminusNum.proof 
208425     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 378.2ns 
208427     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
211554     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.13s 
211554     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmod_pulloutminusNum 
212568     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmod_pulloutminusNum 
212573     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.82ms 
212575     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmod_pulloutminusDenom.proof 
212575     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 100.5ns 
212576     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
215739     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.16s 
215739     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmod_pulloutminusDenom 
216741     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmod_pulloutminusDenom 
216747     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.53ms 
216749     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmodUnique1.proof 
216749     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 119.8ns 
216750     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
219860     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.11s 
219860     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmodUnique1 
220848     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmodUnique1 
220969     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 110.04ms 
220971     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmodUnique2.proof 
220972     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 324.8ns 
220973     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
224080     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.11s 
224081     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmodUnique2 
225070     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmodUnique2 
225199     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 117.98ms 
225202     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_intDivRem.proof 
225203     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 367.6ns 
225204     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
228243     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.04s 
228244     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: intDivRem 
229261     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: intDivRem 
229266     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.09ms 
229268     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmodjmod.proof 
229269     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 279.7ns 
229270     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
232398     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.13s 
232398     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmodjmod 
233398     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmodjmod 
233453     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 48.05ms 
233456     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmodDivisible.proof 
233456     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 493.81ns 
233457     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
236490     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.03s 
236491     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmodDivisible 
237467     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmodDivisible 
237510     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 39.47ms 
237512     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmodDivisibleRep.proof 
237512     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 97.9ns 
237513     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
240564     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.05s 
240564     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmodDivisibleRep 
241562     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmodDivisibleRep 
241567     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.66ms 
241572     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdivAddMultDenom.proof 
241573     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 239.4ns 
241574     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
244616     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.04s 
244616     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdivAddMultDenom 
245586     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdivAddMultDenom 
245823     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 223.78ms 
245825     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmodAltZero.proof 
245826     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 166.9ns 
245827     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
248975     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.15s 
248976     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmodAltZero 
249971     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmodAltZero 
249992     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 17.55ms 
249993     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmodAddMultDenomZero.proof 
249993     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 99.1ns 
249994     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
253089     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.1s 
253090     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmodAddMultDenomZero 
254092     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmodAddMultDenomZero 
254103     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 9.33ms 
254105     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_polyDiv_zero.proof 
254105     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 88ns 
254106     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
257139     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.03s 
257140     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: polyDiv_zero 
258088     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: polyDiv_zero 
258113     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 21.68ms 
258115     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_polyMod_ltdivDenom.proof 
258115     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 81.5ns 
258116     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
261214     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.1s 
261214     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: polyMod_ltdivDenom 
262193     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: polyMod_ltdivDenom 
262211     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 11.17ms 
262214     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_empty.proof 
262214     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 85.9ns 
262215     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
265237     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.02s 
265237     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_empty 
266191     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_empty 
266196     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.26ms 
266197     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_induction_upper.proof 
266198     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 87.3ns 
266198     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
269233     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.03s 
269233     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_upper 
270198     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_induction_upper 
270204     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.82ms 
270205     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_induction_lower.proof 
270205     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 84.9ns 
270206     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
273180     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.97s 
273180     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_lower 
274160     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_induction_lower 
274195     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 31.04ms 
274196     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_bounds.proof 
274196     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 87.6ns 
274197     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
277256     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.06s 
277256     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_bounds 
278240     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_bounds 
278265     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 21.15ms 
278267     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_bounds2.proof 
278267     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 149.4ns 
278268     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
281288     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.02s 
281289     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_bounds2 
282303     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_bounds2 
282327     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 20.18ms 
282328     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_induction_upper2.proof 
282328     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 82.2ns 
282329     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
285421     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.09s 
285422     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_upper2 
286431     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_induction_upper2 
286435     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.34ms 
286437     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_induction_upper_concrete.proof 
286437     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 81.8ns 
286438     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
289545     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.11s 
289546     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_upper_concrete 
290535     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_induction_upper_concrete 
290541     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.06ms 
290543     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_induction_upper_concrete_2.proof 
290543     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 102.6ns 
290544     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
293620     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.08s 
293621     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_upper_concrete_2 
294592     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_induction_upper_concrete_2 
294600     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 5.97ms 
294603     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_induction_upper2_concrete.proof 
294603     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 229.5ns 
294604     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
297665     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.06s 
297665     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_upper2_concrete 
298650     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_induction_upper2_concrete 
298654     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.07ms 
298656     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_induction_lower_concrete.proof 
298656     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 77.4ns 
298657     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
301724     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.07s 
301724     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_lower_concrete 
302688     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_induction_lower_concrete 
302691     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 951.11ns 
302693     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_induction_lower2.proof 
302693     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 96.4ns 
302694     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
305745     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.05s 
305745     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_lower2 
306727     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_induction_lower2 
306732     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.24ms 
306734     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_induction_lower2_concrete.proof 
306734     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 112.4ns 
306735     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
309809     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.07s 
309809     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_lower2_concrete 
310769     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_induction_lower2_concrete 
310773     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.61ms 
310775     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_positive.proof 
310775     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 81.4ns 
310776     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
313825     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.05s 
313825     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_positive 
314819     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_positive 
314880     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 58.24ms 
314882     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_upper_bound.proof 
314882     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 85.7ns 
314883     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
317902     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.02s 
317902     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_upper_bound 
318878     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_upper_bound 
318928     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 47.02ms 
318930     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_lower_bound.proof 
318930     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 89.2ns 
318931     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
322006     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.07s 
322006     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_lower_bound 
323015     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_lower_bound 
323067     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 48.54ms 
323070     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_positive_lower_bound_element.proof 
323070     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 94.9ns 
323071     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
326107     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.04s 
326108     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_positive_lower_bound_element 
327101     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_positive_lower_bound_element 
327175     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 69.5ms 
327177     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_sub_same_index.proof 
327177     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 102.2ns 
327178     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
330254     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.08s 
330254     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_sub_same_index 
331240     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_sub_same_index 
331287     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 43.11ms 
331288     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_less_same_index.proof 
331288     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 84.7ns 
331289     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
334308     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.02s 
334308     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_less_same_index 
335302     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_less_same_index 
335385     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 77.37ms 
335388     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_equal_except_one_index.proof 
335388     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 336.1ns 
335390     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
338451     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.06s 
338451     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_equal_except_one_index 
339430     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_equal_except_one_index 
339474     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 40.33ms 
339476     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_is_max.proof 
339476     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 87.7ns 
339477     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
342487     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.01s 
342487     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_is_max 
343484     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_is_max 
343514     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 27.09ms 
343516     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_is_max2.proof 
343516     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 75ns 
343517     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
346637     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.12s 
346637     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_is_max2 
347638     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_is_max2 
347675     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 33.19ms 
347677     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_is_max3.proof 
347677     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 87.8ns 
347678     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
350719     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.04s 
350719     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_is_max3 
351687     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_is_max3 
351715     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 24.93ms 
351719     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_is_max4.proof 
351719     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 92.9ns 
351720     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
354801     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.08s 
354801     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_is_max4 
355783     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_is_max4 
355823     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 35.48ms 
355826     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_lt_max.proof 
355826     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 227.6ns 
355831     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
358843     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.01s 
358843     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_lt_max 
359832     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_lt_max 
359870     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 34.09ms 
359871     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_lt_max2.proof 
359871     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 95.7ns 
359872     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
362987     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.11s 
362987     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_lt_max2 
363948     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_lt_max2 
363986     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 34.15ms 
363990     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_lt_max3.proof 
363990     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 108.3ns 
363991     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
367024     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.03s 
367025     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_lt_max3 
368009     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_lt_max3 
368044     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 31.89ms 
368046     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_lt_max4.proof 
368046     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 97.2ns 
368047     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
371126     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.08s 
371126     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_lt_max4 
372084     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_lt_max4 
372115     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 28.23ms 
372117     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_gt0.proof 
372117     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 76.8ns 
372119     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
375214     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.1s 
375215     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_gt0 
376212     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_gt0 
376247     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 31ms 
376248     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_gt0_alt.proof 
376249     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 90ns 
376249     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
379298     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.05s 
379298     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_gt0_alt 
380255     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_gt0_alt 
380291     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 32.84ms 
380293     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_add_concrete.proof 
380293     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 85.4ns 
380294     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
383359     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.06s 
383359     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_add_concrete 
384367     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_add_concrete 
384379     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 9.55ms 
384383     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bprod/Taclet_bprod_all_positive.proof 
384383     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 240ns 
384384     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
387414     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.03s 
387414     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bprod_all_positive 
388391     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bprod_all_positive 
388416     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 22.08ms 
388418     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bprod/Taclet_bprod_split.proof 
388418     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 69.9ns 
388419     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
391469     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.05s 
391470     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bprod_split 
392464     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bprod_split 
392469     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.58ms 
392472     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powConcrete0.proof 
392472     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 246.6ns 
392473     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
395480     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.01s 
395481     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powConcrete0 
396494     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powConcrete0 
396499     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 872.71ns 
396500     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powConcrete1.proof 
396500     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 78.2ns 
396501     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
399564     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.06s 
399564     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powConcrete1 
400583     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powConcrete1 
400585     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.03ms 
400587     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powSplitFactor.proof 
400587     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 68.6ns 
400588     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
403674     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.09s 
403674     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powSplitFactor 
404663     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powSplitFactor 
404673     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 7.09ms 
404674     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powAdd.proof 
404674     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 92.9ns 
404675     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
407739     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.06s 
407739     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powAdd 
408721     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powAdd 
408730     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 5.94ms 
408732     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powMono.proof 
408732     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 88.9ns 
408733     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
411850     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.12s 
411853     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powMono 
412844     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powMono 
412861     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 14.64ms 
412863     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powMonoConcrete.proof 
412863     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 86.7ns 
412864     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
415918     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.05s 
415919     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powMonoConcrete 
416895     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powMonoConcrete 
416900     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.66ms 
416902     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powMonoConcreteRight.proof 
416902     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 190.6ns 
416903     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
419974     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.07s 
419974     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powMonoConcreteRight 
420948     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powMonoConcreteRight 
420950     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 789.71ns 
420952     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powPositive.proof 
420953     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 94.7ns 
420953     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
423987     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.03s 
423988     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powPositive 
424950     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powPositive 
424958     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 5.48ms 
424959     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powPositiveConcrete.proof 
424959     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 78.5ns 
424960     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
427996     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.04s 
427996     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powPositiveConcrete 
428993     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powPositiveConcrete 
428996     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.06ms 
428998     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powGeq1Concrete.proof 
428998     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 65.5ns 
428999     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
431989     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.99s 
431989     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powGeq1Concrete 
432981     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powGeq1Concrete 
432983     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 775.21ns 
432985     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_pow2InIntLower.proof 
432985     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 76.5ns 
432986     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
435998     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.01s 
435999     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: pow2InIntLower 
436956     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: pow2InIntLower 
436960     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.03ms 
436963     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_pow2InIntUpper.proof 
436963     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 190.1ns 
436964     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
440005     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.04s 
440005     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: pow2InIntUpper 
440980     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: pow2InIntUpper 
440985     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.92ms 
440987     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logSelfConcrete.proof 
440987     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 80.1ns 
440987     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
444034     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.05s 
444034     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logSelfConcrete 
445035     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logSelfConcrete 
445047     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 10.22ms 
445049     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_log1Concrete.proof 
445049     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 82.5ns 
445050     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
448122     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.07s 
448122     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: log1Concrete 
449121     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: log1Concrete 
449126     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.37ms 
449128     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logProduct.proof 
449128     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 79.6ns 
449129     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
452145     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.02s 
452145     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logProduct 
453130     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logProduct 
453140     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 7.33ms 
453142     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logTimesBaseConcrete.proof 
453143     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 240.2ns 
453144     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
456114     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.97s 
456114     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logTimesBaseConcrete 
457102     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logTimesBaseConcrete 
457108     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.11ms 
457109     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logProdIdentity.proof 
457109     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 60.9ns 
457110     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
460217     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.11s 
460217     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logProdIdentity 
461212     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logProdIdentity 
461236     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 19.26ms 
461238     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logProdIdentityConcrete.proof 
461238     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 63ns 
461239     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
464310     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.07s 
464311     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logProdIdentityConcrete 
465253     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logProdIdentityConcrete 
465258     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.6ms 
465259     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logPowIdentity.proof 
465259     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 81.6ns 
465260     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
468289     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.03s 
468289     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logPowIdentity 
469276     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logPowIdentity 
469281     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.28ms 
469282     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logPowIdentityConcrete.proof 
469282     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 72ns 
469283     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
472374     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.09s 
472374     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logPowIdentityConcrete 
473331     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logPowIdentityConcrete 
473336     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.96ms 
473338     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logPositive.proof 
473338     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 84.4ns 
473339     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
476394     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.06s 
476395     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logPositive 
477398     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logPositive 
477426     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 23.28ms 
477428     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logPositiveConcrete.proof 
477428     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 113.6ns 
477429     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
480519     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.09s 
480519     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logPositiveConcrete 
481492     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logPositiveConcrete 
481497     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 819.71ns 
481500     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logMono.proof 
481500     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 80.4ns 
481501     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
484554     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.05s 
484555     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logMono 
485548     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logMono 
485606     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 53.06ms 
485607     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logMonoConcrete.proof 
485608     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 76.9ns 
485608     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
488655     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.05s 
488656     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logMonoConcrete 
489622     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logMonoConcrete 
489627     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.29ms 
489628     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powLogLess.proof 
489628     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 64ns 
489629     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
492669     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.04s 
492669     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powLogLess 
493628     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powLogLess 
493660     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 28.04ms 
493661     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powLogMore2.proof 
493661     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 74.6ns 
493662     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
496703     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.04s 
496704     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powLogMore2 
497697     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powLogMore2 
497735     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 32.68ms 
497738     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logLessThanPow.proof 
497738     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 236ns 
497739     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
500745     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.01s 
500745     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logLessThanPow 
501737     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logLessThanPow 
501773     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 30.36ms 
501775     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logLessThanPowConcrete.proof 
501775     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 75.4ns 
501776     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
504830     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.05s 
504830     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logLessThanPowConcrete 
505806     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logLessThanPowConcrete 
505809     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 759.21ns 
505811     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logSqueeze.proof 
505811     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 61.2ns 
505812     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
508862     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.05s 
508862     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logSqueeze 
509861     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logSqueeze 
509869     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 5.53ms 
509871     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/booleanRules/Taclet_ifthenelse_equals.proof 
509871     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 123.3ns 
509872     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
512976     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.1s 
512977     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: ifthenelse_equals 
513994     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: ifthenelse_equals 
513998     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.7ms 
513999     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/booleanRules/Taclet_ifthenelse_equals_1.proof 
513999     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 74.6ns 
514000     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
517112     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.11s 
517113     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: ifthenelse_equals_1 
518129     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: ifthenelse_equals_1 
518132     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.1ms 
518134     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/booleanRules/Taclet_ifthenelse_equals_2.proof 
518134     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 63ns 
518135     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
521190     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.06s 
521190     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: ifthenelse_equals_2 
522205     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: ifthenelse_equals_2 
522208     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.22ms 
522210     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/locSet/Taclet_disjointWithSingleton1.proof 
522210     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 80.4ns 
522210     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
525266     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.06s 
525266     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: disjointWithSingleton1 
526274     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: disjointWithSingleton1 
526279     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.27ms 
526280     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/locSet/Taclet_disjointWithSingleton2.proof 
526280     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 65.2ns 
526281     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
529365     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.08s 
529365     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: disjointWithSingleton2 
530374     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: disjointWithSingleton2 
530378     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.02ms 
530380     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/locSet/Taclet_disjointArrayRanges.proof 
530380     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 143ns 
530381     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
533437     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.06s 
533437     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: disjointArrayRanges 
534438     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: disjointArrayRanges 
534452     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 10.69ms 
534454     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/locSet/Taclet_disjointArrayRangeAllFields1.proof 
534454     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 58.3ns 
534454     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
537501     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.05s 
537501     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: disjointArrayRangeAllFields1 
538492     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: disjointArrayRangeAllFields1 
538510     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 15.12ms 
538512     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/locSet/Taclet_disjointArrayRangeAllFields2.proof 
538512     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 77.6ns 
538513     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
541569     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.06s 
541569     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: disjointArrayRangeAllFields2 
542568     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: disjointArrayRangeAllFields2 
542585     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 14.77ms 
542587     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqSelfDefinition.proof 
542587     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 80.5ns 
542588     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
545638     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.05s 
545638     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqSelfDefinition 
546656     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqSelfDefinition 
546679     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 18.21ms 
546680     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqOutsideValue.proof 
546680     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 81.3ns 
546681     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
549727     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.05s 
549728     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqOutsideValue 
550754     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqOutsideValue 
550760     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.78ms 
550761     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_castedGetAny.proof 
550762     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 75.9ns 
550762     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
553848     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.09s 
553848     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: castedGetAny 
554857     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: castedGetAny 
554865     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 6.51ms 
554867     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqGetAlphaCast.proof 
554867     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 81ns 
554867     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
557905     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.04s 
557905     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqGetAlphaCast 
558904     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqGetAlphaCast 
558910     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.24ms 
558912     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqSingleton.proof 
558912     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 220.9ns 
558914     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
561984     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.07s 
561984     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqSingleton 
563002     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqSingleton 
563006     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.84ms 
563008     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqSingletonConcrete.proof 
563008     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 62.6ns 
563008     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
566034     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.03s 
566034     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqSingletonConcrete 
567031     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqSingletonConcrete 
567034     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.3ms 
567036     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqConcat.proof 
567036     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 76ns 
567037     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
570071     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.03s 
570071     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqConcat 
571077     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqConcat 
571092     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 12.52ms 
571093     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqSub.proof 
571093     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 112.2ns 
571094     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
574168     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.07s 
574168     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqSub 
575182     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqSub 
575188     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.62ms 
575189     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqReverse.proof 
575189     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 74.5ns 
575190     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
578236     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.05s 
578237     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqReverse 
579244     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqReverse 
579253     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 7.01ms 
579255     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqEmpty.proof 
579255     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 79.7ns 
579255     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
582322     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.07s 
582322     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqEmpty 
583338     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqEmpty 
583341     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.08ms 
583342     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqSingleton.proof 
583342     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 75.1ns 
583343     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
586421     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.08s 
586421     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqSingleton 
587429     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqSingleton 
587431     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 942.31ns 
587433     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqConcat.proof 
587433     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 74ns 
587434     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
590518     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.08s 
590519     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqConcat 
591533     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqConcat 
591538     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.33ms 
591540     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqSub.proof 
591540     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 98.5ns 
591541     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
594591     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.05s 
594592     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqSub 
595587     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqSub 
595591     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.98ms 
595593     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqReverse.proof 
595593     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 70.1ns 
595593     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
598635     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.04s 
598635     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqReverse 
599634     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqReverse 
599638     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.27ms 
599640     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_equalityToSeqGetAndSeqLenLeft.proof 
599640     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 63.5ns 
599641     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
602690     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.05s 
602690     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: equalityToSeqGetAndSeqLenLeft 
603711     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: equalityToSeqGetAndSeqLenLeft 
603715     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.84ms 
603716     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_equalityToSeqGetAndSeqLenRight.proof 
603716     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 78.4ns 
603717     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
606787     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.07s 
606787     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: equalityToSeqGetAndSeqLenRight 
607794     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: equalityToSeqGetAndSeqLenRight 
607802     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 5.38ms 
607803     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqSingletonEQ.proof 
607803     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 62.5ns 
607804     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
610860     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.06s 
610860     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqSingletonEQ 
611870     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqSingletonEQ 
611876     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.1ms 
611878     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqConcatEQ.proof 
611878     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 94.4ns 
611879     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
614936     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.06s 
614936     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqConcatEQ 
615946     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqConcatEQ 
615963     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 14.43ms 
615965     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqSubEQ.proof 
615965     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 65.3ns 
615965     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
618992     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.03s 
618993     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqSubEQ 
619956     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqSubEQ 
619959     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.04ms 
619960     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqReverseEQ.proof 
619960     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 76.6ns 
619961     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
623071     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.11s 
623072     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqReverseEQ 
624051     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqReverseEQ 
624062     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 7.71ms 
624063     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqEmptyEQ.proof 
624063     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 82.3ns 
624064     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
627140     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.08s 
627140     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqEmptyEQ 
628151     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqEmptyEQ 
628154     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.34ms 
628156     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqSingletonEQ.proof 
628156     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 63.2ns 
628156     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
631211     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.05s 
631211     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqSingletonEQ 
632219     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqSingletonEQ 
632223     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.44ms 
632225     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqConcatEQ.proof 
632225     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 101.9ns 
632226     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
635261     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.04s 
635261     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqConcatEQ 
636262     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqConcatEQ 
636269     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.61ms 
636271     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqSubEQ.proof 
636271     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 74.8ns 
636271     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
639302     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.03s 
639303     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqSubEQ 
640313     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqSubEQ 
640318     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.23ms 
640320     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqReverseEQ.proof 
640320     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 141.7ns 
640321     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
643435     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.11s 
643435     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqReverseEQ 
644449     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqReverseEQ 
644454     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.61ms 
644455     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqDefEQ.proof 
644455     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 55.8ns 
644456     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
647536     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.08s 
647537     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqDefEQ 
648555     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqDefEQ 
648561     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.86ms 
648562     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqDefEQ.proof 
648562     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 83.3ns 
648564     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
651625     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.06s 
651625     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqDefEQ 
652675     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqDefEQ 
652682     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 5.41ms 
652686     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqConcatWithSeqEmpty1.proof 
652686     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 109.6ns 
652687     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
655755     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.07s 
655755     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqConcatWithSeqEmpty1 
656772     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqConcatWithSeqEmpty1 
656795     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 19.75ms 
656796     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqConcatWithSeqEmpty2.proof 
656796     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 78.1ns 
656797     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
659908     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.11s 
659909     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqConcatWithSeqEmpty2 
660922     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqConcatWithSeqEmpty2 
660945     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 21.07ms 
660947     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqReverseOfSeqEmpty.proof 
660947     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 74ns 
660948     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
664015     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.07s 
664015     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqReverseOfSeqEmpty 
665021     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqReverseOfSeqEmpty 
665035     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 12.05ms 
665037     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_subSeqComplete.proof 
665037     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 71ns 
665038     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
668075     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.04s 
668076     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: subSeqComplete 
669092     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: subSeqComplete 
669108     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 12.96ms 
669109     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_subSeqTailR.proof 
669110     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 76.7ns 
669110     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
672148     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.04s 
672148     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: subSeqTailR 
673154     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: subSeqTailR 
673190     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 33.39ms 
673192     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_subSeqTailL.proof 
673192     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 80.9ns 
673193     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
676246     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.05s 
676247     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: subSeqTailL 
677254     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: subSeqTailL 
677292     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 35.28ms 
677293     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_subSeqTailEQR.proof 
677294     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 79.8ns 
677294     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
680354     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.06s 
680354     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: subSeqTailEQR 
681369     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: subSeqTailEQR 
681403     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 31.32ms 
681405     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_subSeqTailEQL.proof 
681405     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 66.5ns 
681406     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
684460     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.05s 
684460     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: subSeqTailEQL 
685462     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: subSeqTailEQL 
685485     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 19.3ms 
685487     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDef_split.proof 
685487     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 79.2ns 
685488     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
688542     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.05s 
688542     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_split 
689581     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDef_split 
689629     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 44ms 
689631     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDef_induction_upper.proof 
689631     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 73.3ns 
689632     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
692739     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.11s 
692740     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_induction_upper 
693744     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDef_induction_upper 
693814     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 65.48ms 
693816     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDef_induction_upper_concrete.proof 
693816     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 78.6ns 
693816     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
696860     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.04s 
696860     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_induction_upper_concrete 
697868     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDef_induction_upper_concrete 
697926     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 54.21ms 
697928     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDef_induction_lower.proof 
697928     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 77.3ns 
697929     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
700982     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.05s 
700982     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_induction_lower 
702022     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDef_induction_lower 
702087     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 60.83ms 
702089     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDef_induction_lower_concrete.proof 
702089     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 74.8ns 
702090     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
705212     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.12s 
705212     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_induction_lower_concrete 
706252     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDef_induction_lower_concrete 
706316     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 60.37ms 
706318     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDef_split_in_three.proof 
706318     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 66.4ns 
706319     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
709428     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.11s 
709428     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_split_in_three 
710461     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDef_split_in_three 
710640     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 170.57ms 
710642     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDef_empty.proof 
710642     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 83.1ns 
710643     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
713763     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.12s 
713763     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_empty 
714775     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDef_empty 
714788     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 11.75ms 
714793     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDef_one_summand.proof 
714793     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 87.5ns 
714794     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
717907     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.11s 
717907     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_one_summand 
718918     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDef_one_summand 
718929     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 8.3ms 
718930     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDef_lower_equals_upper.proof 
718931     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 139.9ns 
718931     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
721973     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.04s 
721973     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_lower_equals_upper 
722979     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDef_lower_equals_upper 
722987     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 5.43ms 
722988     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDefOfSeq.proof 
722988     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 74.1ns 
722989     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
726080     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.09s 
726081     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDefOfSeq 
727132     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDefOfSeq 
727159     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 22.75ms 
727160     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqSelfDefinitionEQ2.proof 
727160     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 71.9ns 
727161     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
730255     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.09s 
730255     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqSelfDefinitionEQ2 
731278     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqSelfDefinitionEQ2 
731298     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 17.55ms 
731300     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_indexOfSeqSingleton.proof 
731300     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 74.4ns 
731301     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
734339     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.04s 
734340     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: indexOfSeqSingleton 
735352     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: indexOfSeqSingleton 
735356     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.56ms 
735359     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_indexOfSeqConcatFirst.proof 
735359     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 80.7ns 
735360     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
738391     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.03s 
738391     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: indexOfSeqConcatFirst 
739401     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: indexOfSeqConcatFirst 
739424     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 20.44ms 
739426     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_indexOfSeqConcatSecond.proof 
739426     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 64.5ns 
739426     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
742576     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.15s 
742576     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: indexOfSeqConcatSecond 
743586     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: indexOfSeqConcatSecond 
743610     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 20.45ms 
743611     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_indexOfSeqSub.proof 
743611     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 79.7ns 
743612     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
746664     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.05s 
746664     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: indexOfSeqSub 
747690     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: indexOfSeqSub 
747719     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 25.55ms 
747721     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfArray2seq.proof 
747721     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 76.7ns 
747722     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
750795     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.07s 
750796     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfArray2seq 
751816     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfArray2seq 
751820     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.51ms 
751821     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getAnyOfArray2seq.proof 
751821     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 60.4ns 
751823     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
754908     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.08s 
754908     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getAnyOfArray2seq 
755924     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getAnyOfArray2seq 
755930     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.49ms 
755932     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfArray2seq.proof 
755932     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 82.8ns 
755933     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
759028     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.09s 
759028     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfArray2seq 
760035     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfArray2seq 
760044     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 6.49ms 
760045     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_getAnyOfNPermInv.proof 
760045     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 71.6ns 
760046     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
763132     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.09s 
763132     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getAnyOfNPermInv 
764172     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getAnyOfNPermInv 
764183     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 8.84ms 
764184     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqNPermRange.proof 
764184     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 61.2ns 
764185     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
767225     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.04s 
767225     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqNPermRange 
768219     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqNPermRange 
768337     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 110.67ms 
768340     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermTrans.proof 
768340     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 244.9ns 
768341     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
771435     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.09s 
771435     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermTrans 
772442     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermTrans 
772479     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 33.36ms 
772482     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermRefl.proof 
772482     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 282.4ns 
772483     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
775519     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.04s 
775519     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermRefl 
776550     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermRefl 
776581     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 27.86ms 
776582     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermSplit.proof 
776583     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 76ns 
776583     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
779611     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.03s 
779612     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermSplit 
780617     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermSplit 
780620     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 380.5ns 
780621     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqNPermRight.proof 
780622     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 76.7ns 
780623     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
783699     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.08s 
783699     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqNPermRight 
784711     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqNPermRight 
785011     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 287.18ms 
785014     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermFromSwap.proof 
785014     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 111ns 
785015     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
788091     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.08s 
788091     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermFromSwap 
789108     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermFromSwap 
789181     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 67.12ms 
789183     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermTransAlt0.proof 
789183     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 66.4ns 
789183     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
792181     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3s 
792181     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermTransAlt0 
793200     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermTransAlt0 
793203     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 451.4ns 
793205     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermTransAlt1.proof 
793205     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 60.8ns 
793205     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
796226     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.02s 
796226     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermTransAlt1 
797237     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermTransAlt1 
797240     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 492.81ns 
797241     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermTransAlt2.proof 
797241     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 77.5ns 
797242     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
800294     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.05s 
800294     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermTransAlt2 
801305     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermTransAlt2 
801308     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 464.5ns 
801309     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermTransAlt3.proof 
801310     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 78.2ns 
801310     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
804369     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.06s 
804370     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermTransAlt3 
805439     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermTransAlt3 
805442     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 679.91ns 
805444     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermForall.proof 
805445     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 236ns 
805446     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
808539     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.09s 
808539     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermForall 
809535     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermForall 
809663     INFO  Test worker     d.u.i.k.s.SMTFocusResults Analyzing unsat core: (L_1 L_3 L_4) 
809683     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 144.78ms 
809685     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermExists.proof 
809685     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 93.5ns 
809687     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
812756     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.07s 
812756     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermExists 
813786     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermExists 
813843     INFO  Test worker     d.u.i.k.s.SMTFocusResults Analyzing unsat core: (L_1 L_3 L_5 L_6 L_7) 
813845     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 57.25ms 
813847     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm2/Taclet_schiffl_lemma_2.proof 
813847     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 63.2ns 
813853     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
816964     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.11s 
816964     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: schiffl_lemma_2 
817996     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: schiffl_lemma_2 
817998     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.1ns 
818036     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 1: 'macro split-prop' 
818096     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 2: 'rule allRight' 
818121     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 3: 'rule allRight' 
818131     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 4: 'macro split-prop' 
818142     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 5: 'rule 'seqPermDefLeft'' 
818146     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 6: 'rule 'andLeft'' 
818147     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 7: 'rule 'exLeft'' 
818152     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 8: 'macro split-prop' 
818159     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 9: 'rule  seqNPermRange' 
818162     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 10: 'instantiate var=iv with='v_x_0' occ=1' 
818169     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 11: 'rule impLeft' 
818173     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 12: 'tryclose branch' 
818398     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 13: 'rule andLeft' 
818400     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 14: 'rule andLeft' 
818401     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 15: 'instantiate var=iv with='v_y_0' occ=1' 
818402     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 16: 'rule impLeft' 
818403     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 17: 'tryclose branch' 
818555     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 18: 'rule andLeft' 
818557     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 19: 'rule andLeft' 
818557     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 20: 'rule seqNPermDefLeft' 
818560     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 21: 'instantiate var=iv with='v_x_0' occ=2' 
818561     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 22: 'rule impLeft' 
818562     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 23: 'tryclose branch' 
818771     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 24: 'rule exLeft' 
818773     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 25: 'rule andLeft' 
818774     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 26: 'rule andLeft' 
818775     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 27: 'instantiate hide var=iv with='v_y_0' occ=2' 
818776     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 28: 'rule impLeft' 
818777     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 29: 'tryclose branch' 
818937     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 30: 'rule exLeft' 
818939     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 31: 'rule andLeft' 
818940     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 32: 'rule andLeft' 
818941     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 33: 'instantiate var=iv with='jv_0' occ=1' 
818943     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 34: 'rule impLeft' 
818943     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 35: 'tryclose branch' 
818952     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 36: 'rule andLeft' 
818954     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 37: 'rule andLeft' 
818955     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 38: 'rule castAdd formula='s_0[jv_0] = v_x_0' occ=0' 
818957     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 39: 'instantiate hide var=iv with='jv_1' occ=1' 
818958     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 40: 'rule impLeft' 
818959     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 41: 'tryclose branch' 
818967     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 42: 'rule andLeft' 
818968     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 43: 'rule andLeft' 
818969     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 44: 'rule castAdd formula='s_0[jv_1] = v_y_0' occ=0' 
818970     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 45: 'instantiate var=iv  with='v_x_0'' 
818970     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 46: 'rule impLeft' 
818971     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 47: 'tryclose branch' 
819148     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 48: 'instantiate var=iv  with='v_y_0'' 
819149     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 49: 'rule impLeft' 
819150     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 50: 'tryclose branch' 
819318     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 51: 'cut 'v_x_0 = v_y_0'' 
819320     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)'' 
819323     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 53: 'rule andRight' 
819325     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 54: 'rule andRight' 
819326     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 55: 'rule andRight' 
819327     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 56: 'rule andRight' 
819328     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 57: 'rule lenOfSwap' 
819328     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 58: 'tryclose branch' 
819333     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 59: 'rule seqNPermSwapNPerm' 
819335     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 60: 'instantiate hide var='iv' with='v_x_0' occ=1' 
819337     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 61: 'instantiate hide var='jv' with='jv_0'' 
819338     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 62: 'rule impLeft' 
819339     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 63: 'tryclose branch' 
819488     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 64: 'tryclose branch' 
819492     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 65: 'rule allRight' 
819494     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 66: 'rule impRight' 
819495     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 67: 'rule andLeft' 
819496     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 68: 'instantiate var=iv with='v_iv_0'' 
819496     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 69: 'rule impLeft' 
819497     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 70: 'tryclose branch' 
819712     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 71: 'rule getOfSwap' 
819713     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 72: 'rule ifthenelse_negated' 
819714     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 73: 'rule ifthenelse_split occ=0' 
819716     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 74: 'rule andLeft' 
819717     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 75: 'rule andLeft' 
819717     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 76: 'rule andLeft' 
819718     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 77: 'rule ifthenelse_split occ=0' 
819719     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 78: 'tryclose branch' 
819868     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 79: 'rule ifthenelse_split occ=0' 
819870     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 80: 'tryclose branch' 
819994     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 81: 'tryclose branch' 
820000     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 82: 'tryclose branch' 
820006     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 83: 'rule getOfSwap' 
820007     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 84: 'rule ifthenelse_negated' 
820008     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 85: 'rule ifthenelse_split occ=0' 
820010     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 86: 'rule andLeft' 
820010     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 87: 'rule andLeft' 
820010     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 88: 'rule andLeft' 
820011     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 89: 'rule ifthenelse_split occ=0' 
820012     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 90: 'tryclose branch' 
820024     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 91: 'tryclose branch' 
820031     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 92: 'tryclose branch' 
820178     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 93: 'rule getOfSwap' 
820180     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 94: 'rule ifthenelse_negated' 
820181     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 95: 'rule ifthenelse_split occ=0' 
820182     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 96: 'rule andLeft' 
820183     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 97: 'rule andLeft' 
820183     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 98: 'rule andLeft' 
820183     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 99: 'rule ifthenelse_split occ=0' 
820185     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 100: 'tryclose branch' 
820254     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 101: 'tryclose branch' 
820262     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 102: 'tryclose branch' 
820381     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 103: 'cut '(int)s_0[v_x_0] = (int)s_0[v_y_0]'' 
820383     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 104: 'rule seqNPermInjective' 
820385     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 105: 'instantiate hide var=iv with='v_x_0'' 
820386     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 106: 'instantiate hide var=jv with='v_y_0'' 
820387     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 107: 'rule impLeft' 
820388     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 108: 'tryclose branch' 
820544     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 109: 'tryclose branch' 
820549     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 110: 'cut '(int)s_0[v_x_0] = v_x_0'' 
820551     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)'' 
820552     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 112: 'rule andRight' 
820553     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 113: 'rule andRight' 
820554     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 114: 'rule andRight' 
820555     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 115: 'rule andRight' 
820555     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 116: 'tryclose branch' 
820566     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 117: 'rule seqNPermSwapNPerm' 
820568     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 118: 'instantiate hide var=iv with='v_y_0'' 
820569     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 119: 'instantiate hide var=jv with='jv_1'' 
820570     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 120: 'tryclose branch' 
820687     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 121: 'rule allRight' 
820689     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 122: 'rule impRight' 
820689     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 123: 'rule andLeft' 
820690     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 124: 'instantiate var=iv with='v_iv_0'' 
820691     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 125: 'rule impLeft' 
820692     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 126: 'tryclose branch' 
820817     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 127: 'rule getOfSwap' 
820818     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 128: 'rule ifthenelse_negated' 
820819     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 129: 'rule ifthenelse_split occ=0' 
820821     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 130: 'rule andLeft' 
820821     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 131: 'rule andLeft' 
820822     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 132: 'rule andLeft' 
820822     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 133: 'rule ifthenelse_split occ=0' 
820824     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 134: 'tryclose branch' 
820927     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 135: 'rule ifthenelse_split occ=0' 
820928     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 136: 'tryclose branch' 
821021     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 137: 'instantiate var=iv with='v_y_0'' 
821021     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 138: 'rule impLeft' 
821022     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 139: 'tryclose branch' 
821027     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 140: 'tryclose branch' 
821032     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 141: 'tryclose branch' 
821037     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 142: 'tryclose branch' 
821186     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 143: 'rule getOfSwap' 
821187     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 144: 'rule ifthenelse_negated' 
821188     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 145: 'rule ifthenelse_split occ=0' 
821189     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 146: 'tryclose branch' 
821204     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 147: 'tryclose branch' 
821318     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 148: 'tryclose branch' 
825865     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 149: 'cut  '(int)s_0[v_y_0] = v_y_0'' 
825869     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)'' 
825875     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 151: 'rule andRight' 
825877     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 152: 'rule andRight' 
825877     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 153: 'rule andRight' 
825878     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 154: 'rule andRight' 
825879     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 155: 'tryclose branch' 
825889     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 156: 'rule seqNPermSwapNPerm' 
825891     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 157: 'instantiate hide var=iv with='v_x_0'' 
825893     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 158: 'instantiate hide var=jv with='jv_0'' 
825894     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 159: 'rule impLeft' 
825895     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 160: 'tryclose branch' 
826022     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 161: 'tryclose branch' 
826027     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 162: 'rule allRight' 
826028     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 163: 'rule impRight' 
826029     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 164: 'rule andLeft' 
826029     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 165: 'instantiate var=iv with='v_iv_0'' 
826030     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 166: 'rule impLeft' 
826031     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 167: 'tryclose branch' 
826153     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 168: 'rule getOfSwap' 
826154     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 169: 'rule ifthenelse_negated' 
826155     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 170: 'rule ifthenelse_split occ=0' 
826157     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 171: 'rule andLeft' 
826157     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 172: 'rule andLeft' 
826158     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 173: 'rule andLeft' 
826158     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 174: 'rule ifthenelse_split occ=0' 
826159     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 175: 'tryclose branch' 
826261     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 176: 'rule ifthenelse_split occ=0' 
826263     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 177: 'tryclose branch' 
826359     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 178: 'tryclose branch' 
826365     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 179: 'tryclose branch' 
826370     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 180: 'rule getOfSwap' 
826371     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 181: 'rule ifthenelse_negated' 
826372     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 182: 'rule ifthenelse_split occ=0' 
826373     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 183: 'tryclose branch' 
826385     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 184: 'tryclose branch' 
826489     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 185: 'rule getOfSwap' 
826490     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 186: 'rule ifthenelse_negated' 
826491     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 187: 'rule ifthenelse_split occ=0' 
826492     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 188: 'tryclose branch' 
826584     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 189: 'tryclose branch' 
826596     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 190: 'cut '(int)s_0[v_x_0]=v_y_0'' 
826597     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)'' 
826599     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 192: 'rule andRight' 
826600     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 193: 'rule andRight' 
826601     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 194: 'rule andRight' 
826602     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 195: 'rule andRight' 
826603     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 196: 'tryclose branch' 
826617     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 197: 'rule seqNPermSwapNPerm' 
826618     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 198: 'instantiate hide var=iv with='jv_0'' 
826620     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 199: 'instantiate hide var=jv with='v_x_0'' 
826620     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 200: 'rule impLeft' 
826621     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 201: 'tryclose branch' 
826733     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 202: 'rule seqNPermSwapNPerm formula='seqNPerm(seqSwap(s_0, jv_0, v_x_0))'' 
826735     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 203: 'instantiate hide var=iv with='jv_0'' 
826737     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 204: 'instantiate hide var=jv with='v_y_0'' 
826738     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 205: 'rule impLeft' 
826739     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 206: 'tryclose branch' 
826853     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 207: 'tryclose branch' 
826859     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 208: 'rule allRight' 
826860     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 209: 'rule impRight' 
826861     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 210: 'rule andLeft' 
826862     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 211: 'instantiate var=iv with='v_iv_0'' 
826863     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 212: 'rule impLeft' 
826864     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 213: 'tryclose branch' 
826989     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 214: 'rule getOfSwap' 
826991     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 215: 'rule ifthenelse_negated' 
826992     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 216: 'rule ifthenelse_split occ=0' 
826994     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 217: 'rule andLeft' 
827000     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 218: 'rule andLeft' 
827002     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 219: 'rule andLeft' 
827005     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 220: 'rule ifthenelse_split occ=0' 
827006     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 221: 'rule getOfSwap' 
827007     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 222: 'rule ifthenelse_negated' 
827008     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 223: 'rule ifthenelse_split occ=0' 
827009     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 224: 'rule andLeft' 
827010     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 225: 'rule andLeft' 
827011     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 226: 'rule andLeft' 
827012     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 227: 'rule ifthenelse_split occ=0' 
827013     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 228: 'tryclose branch' 
827220     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 229: 'rule ifthenelse_split occ=0' 
827222     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 230: 'tryclose branch' 
827229     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 231: 'tryclose branch' 
827329     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 232: 'tryclose branch' 
827433     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 233: 'rule ifthenelse_split' 
827435     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 234: 'rule getOfSwap' 
827436     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 235: 'rule ifthenelse_negated' 
827437     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 236: 'rule ifthenelse_split occ=0' 
827438     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 237: 'rule andLeft' 
827439     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 238: 'rule andLeft' 
827439     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 239: 'rule andLeft' 
827440     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 240: 'rule ifthenelse_split occ=0' 
827441     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 241: 'tryclose branch' 
827551     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 242: 'tryclose branch' 
827559     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 243: 'tryclose branch' 
827675     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 244: 'rule getOfSwap' 
827676     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 245: 'rule ifthenelse_negated' 
827677     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 246: 'rule ifthenelse_split occ=0' 
827679     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 247: 'rule andLeft' 
827680     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 248: 'rule andLeft' 
827680     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 249: 'rule andLeft' 
827681     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 250: 'rule ifthenelse_split occ=0' 
827682     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 251: 'tryclose branch' 
827689     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 252: 'rule ifthenelse_split occ=0' 
827690     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 253: 'tryclose branch' 
827791     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 254: 'tryclose branch' 
827798     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 255: 'tryclose branch' 
827806     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 256: 'tryclose branch' 
827938     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 257: 'rule getOfSwap' 
827940     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 258: 'rule ifthenelse_negated' 
827940     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 259: 'rule ifthenelse_split occ=0' 
827942     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 260: 'rule andLeft' 
827942     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 261: 'rule andLeft' 
827943     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 262: 'rule andLeft' 
827944     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 263: 'rule ifthenelse_split occ=0' 
827945     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 264: 'tryclose branch' 
828022     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 265: 'rule ifthenelse_split occ=0' 
828025     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 266: 'rule getOfSwap' 
828026     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 267: 'rule ifthenelse_negated' 
828027     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 268: 'rule ifthenelse_split occ=0' 
828028     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 269: 'tryclose branch' 
828036     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 270: 'tryclose branch' 
828045     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 271: 'tryclose branch' 
828198     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 272: 'tryclose branch' 
828309     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 273: 'rule getOfSwap' 
828310     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 274: 'rule ifthenelse_negated' 
828311     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 275: 'rule ifthenelse_split occ=0' 
828312     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 276: 'tryclose branch' 
828520     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 277: 'tryclose branch' 
828634     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 278: 'cut 'int::seqGet(s_0, v_y_0)=v_x_0'' 
828635     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 279: 'tryclose branch' 
832350     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 280: 'rule seqNPermSwapNPerm' 
832356     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 281: 'instantiate hide var=iv with='jv_1'' 
832357     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 282: 'instantiate hide var=jv with='v_y_0'' 
832358     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 283: 'rule impLeft' 
832358     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 284: 'tryclose branch' 
832507     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 285: 'rule seqNPermSwapNPerm formula='seqNPerm(seqSwap(s_0,jv_1,v_y_0))'' 
832508     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 286: 'instantiate hide var=iv with='jv_1'' 
832510     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 287: 'instantiate hide var=jv with='v_x_0'' 
832510     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 288: 'rule impLeft' 
832511     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 289: 'tryclose branch' 
832643     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 290: 'tryclose branch' 
836248     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 291: 'tryclose branch' 
840124     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 292: 'rule seqNPermSwapNPerm formula='seqNPerm(s_0)'' 
840130     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 293: 'instantiate hide var=iv with='v_x_0'' 
840131     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 294: 'instantiate hide var=jv with='jv_0'' 
840132     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 295: 'rule impLeft' 
840133     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 296: 'tryclose branch' 
840277     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 297: 'rule seqNPermSwapNPerm formula='seqNPerm(seqSwap(s_0,v_x_0,jv_0))'' 
840278     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 298: 'instantiate hide var=iv with='v_y_0'' 
840279     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 299: 'instantiate hide var=jv with='jv_1'' 
840280     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)' ...' 
840282     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 301: 'tryclose branch' 
841697     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm2/Taclet_schiffl_thm_1.proof 
841697     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 106.3ns 
841698     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
844879     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.18s 
844879     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: schiffl_thm_1 
845909     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: schiffl_thm_1 
845911     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 9.3ns 
845911     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 1: 'macro split-prop' 
845922     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 2: 'rule schiffl_lemma_2 formula='seqPerm(f_s, f_t)'' 
845935     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 3: 'instantiate hide var=x with='f_x'' 
845938     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 4: 'instantiate hide var=y with='f_y'' 
845940     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 5: 'rule impLeft' 
845940     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 6: 'tryclose branch' 
845946     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 7: 'rule exLeft' 
845948     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 8: 'macro split-prop' 
845952     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 9: 'rule seqPermDef occ=1' 
845955     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 10: 'rule andRight' 
845956     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 11: 'tryclose branch' 
845969     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 12: 'instantiate hide var=s with='r_0'' 
845971     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 13: 'rule andRight' 
845971     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 14: 'tryclose branch' 
846039     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 15: 'rule allRight' 
846040     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 16: 'rule impRight' 
846041     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 17: 'instantiate hide var=iv with='iv_0'' 
846041     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 18: 'rule impLeft' 
846042     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 19: 'tryclose branch' 
846126     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 20: 'rule andLeft' 
846126     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 21: 'rule seqNPermRange' 
846128     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 22: 'instantiate hide var=iv with='iv_0'' 
846129     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 23: 'rule impLeft' 
846130     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 24: 'tryclose branch' 
846134     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 25: 'rule andLeft' 
846135     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 26: 'rule andLeft' 
846135     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 27: 'rule seqNPermRange' 
846137     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 28: 'instantiate hide var=iv with='f_x'' 
846138     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 29: 'rule impLeft' 
846139     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 30: 'tryclose branch' 
846245     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 31: 'rule andLeft' 
846246     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 32: 'rule andLeft' 
846247     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 33: 'rule seqNPermRange' 
846248     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 34: 'instantiate hide var=iv with='f_y'' 
846249     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 35: 'rule impLeft' 
846250     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 36: 'tryclose branch' 
846364     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 37: 'rule andLeft' 
846366     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 38: 'rule andLeft' 
846366     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 39: 'rule getOfSeqDef occ=0' 
846367     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 40: 'rule getOfSeqDef' 
846368     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 41: 'rule ifthenelse_split occ=0' 
846369     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 42: 'rule andLeft occ=0' 
846370     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 43: 'rule sub_zero_2 occ=0' 
846370     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 44: 'rule ifthenelse_split occ=2' 
846372     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 45: 'rule andLeft' 
846372     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 46: 'rule sub_zero_2 occ=0' 
846373     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 47: 'rule add_zero_right occ=0' 
846373     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 48: 'rule add_zero_right occ=0' 
846374     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 49: 'rule add_zero_right occ=0' 
846375     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 50: 'rule add_zero_right occ=0' 
846376     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 51: 'rule add_zero_right occ=0' 
846376     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 52: 'rule add_zero_right occ=0' 
846377     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 53: 'rule ifthenelse_split occ=0' 
846378     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 54: 'rule ifthenelse_split occ=0' 
846380     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 55: 'tryclose branch' 
846383     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 56: 'tryclose branch' 
846423     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 57: 'rule ifthenelse_split occ=0' 
846424     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 58: 'tryclose branch' 
846495     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 59: 'rule ifthenelse_split occ=0' 
846497     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 60: 'rule seqNPermInjective' 
846499     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 61: 'instantiate hide var=iv with='iv_0'' 
846500     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 62: 'instantiate hide var=jv with='f_y'' 
846501     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 63: 'rule impLeft' 
846502     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 64: 'tryclose branch' 
846558     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 65: 'tryclose branch' 
846561     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 66: 'rule ifthenelse_split occ=0' 
846563     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 67: 'rule seqNPermInjective' 
846565     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 68: 'instantiate hide var=iv with='iv_0'' 
846566     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 69: 'instantiate hide var=jv with='f_x'' 
846567     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 70: 'rule impLeft' 
846568     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 71: 'tryclose branch' 
846626     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 72: 'tryclose branch' 
846630     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 73: 'tryclose branch' 
846633     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 74: 'tryclose branch' 
846704     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 75: 'tryclose branch' 
846776     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_eqSameSeq.proof 
846776     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 281.7ns 
846777     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
849954     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.18s 
849954     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: eqSameSeq 
851044     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: eqSameSeq 
851094     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 45.85ms