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

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

tests
0

failures
0

ignored
10m31.32s

duration
100%

successful

Tests

Test Method name Duration Result
powPositive data()[100] 3.065s passed
powPositiveConcrete data()[101] 3.031s passed
powGeq1Concrete data()[102] 3.030s passed
pow2InIntLower data()[103] 3.060s passed
pow2InIntUpper data()[104] 3.042s passed
logSelfConcrete data()[105] 3.046s passed
log1Concrete data()[106] 3.083s passed
logProduct data()[107] 3.053s passed
logTimesBaseConcrete data()[108] 3.041s passed
logProdIdentity data()[109] 3.062s passed
moduloByteIsInByte data()[10] 3.125s passed
logProdIdentityConcrete data()[110] 3.044s passed
logPowIdentity data()[111] 3.032s passed
logPowIdentityConcrete data()[112] 3.057s passed
logPositive data()[113] 3.049s passed
logPositiveConcrete data()[114] 3.049s passed
logMono data()[115] 3.076s passed
logMonoConcrete data()[116] 3.036s passed
powLogLess data()[117] 3.076s passed
powLogMore2 data()[118] 3.055s passed
logLessThanPow data()[119] 3.079s passed
moduloCharIsInChar data()[11] 3.117s passed
logLessThanPowConcrete data()[120] 3.039s passed
logSqueeze data()[121] 3.041s passed
ifthenelse_equals data()[122] 3.060s passed
ifthenelse_equals_1 data()[123] 3.040s passed
ifthenelse_equals_2 data()[124] 3.052s passed
disjointWithSingleton1 data()[125] 3.040s passed
disjointWithSingleton2 data()[126] 3.059s passed
disjointArrayRanges data()[127] 3.045s passed
disjointArrayRangeAllFields1 data()[128] 3.088s passed
disjointArrayRangeAllFields2 data()[129] 3.049s passed
div_unique1 data()[12] 3.148s passed
seqSelfDefinition data()[130] 3.066s passed
seqOutsideValue data()[131] 3.072s passed
castedGetAny data()[132] 3.054s passed
seqGetAlphaCast data()[133] 3.071s passed
getOfSeqSingleton data()[134] 3.043s passed
getOfSeqSingletonConcrete data()[135] 3.054s passed
getOfSeqConcat data()[136] 3.067s passed
getOfSeqSub data()[137] 3.069s passed
getOfSeqReverse data()[138] 3.073s passed
lenOfSeqEmpty data()[139] 3.083s passed
div_unique2 data()[13] 3.180s passed
lenOfSeqSingleton data()[140] 3.054s passed
lenOfSeqConcat data()[141] 3.066s passed
lenOfSeqSub data()[142] 3.061s passed
lenOfSeqReverse data()[143] 3.048s passed
equalityToSeqGetAndSeqLenLeft data()[144] 3.076s passed
equalityToSeqGetAndSeqLenRight data()[145] 3.161s passed
getOfSeqSingletonEQ data()[146] 3.040s passed
getOfSeqConcatEQ data()[147] 3.069s passed
getOfSeqSubEQ data()[148] 3.057s passed
getOfSeqReverseEQ data()[149] 3.079s passed
div_exists data()[14] 3.263s passed
lenOfSeqEmptyEQ data()[150] 3.069s passed
lenOfSeqSingletonEQ data()[151] 3.039s passed
lenOfSeqConcatEQ data()[152] 3.058s passed
lenOfSeqSubEQ data()[153] 3.058s passed
lenOfSeqReverseEQ data()[154] 3.058s passed
getOfSeqDefEQ data()[155] 3.061s passed
lenOfSeqDefEQ data()[156] 3.062s passed
seqConcatWithSeqEmpty1 data()[157] 3.064s passed
seqConcatWithSeqEmpty2 data()[158] 3.082s passed
seqReverseOfSeqEmpty data()[159] 3.071s passed
div_one data()[15] 3.094s passed
subSeqComplete data()[160] 3.081s passed
subSeqTailR data()[161] 3.082s passed
subSeqTailL data()[162] 3.080s passed
subSeqTailEQR data()[163] 3.080s passed
subSeqTailEQL data()[164] 3.072s passed
seqDef_split data()[165] 3.100s passed
seqDef_induction_upper data()[166] 3.140s passed
seqDef_induction_upper_concrete data()[167] 3.106s passed
seqDef_induction_lower data()[168] 3.103s passed
seqDef_induction_lower_concrete data()[169] 3.111s passed
jdiv_one data()[16] 3.121s passed
seqDef_split_in_three data()[170] 3.176s passed
seqDef_empty data()[171] 3.098s passed
seqDef_one_summand data()[172] 3.077s passed
seqDef_lower_equals_upper data()[173] 3.066s passed
seqDefOfSeq data()[174] 3.076s passed
seqSelfDefinitionEQ2 data()[175] 3.074s passed
indexOfSeqSingleton data()[176] 3.060s passed
indexOfSeqConcatFirst data()[177] 3.076s passed
indexOfSeqConcatSecond data()[178] 3.098s passed
indexOfSeqSub data()[179] 3.075s passed
div_zero data()[17] 3.158s passed
lenOfArray2seq data()[180] 3.060s passed
getAnyOfArray2seq data()[181] 3.058s passed
getOfArray2seq data()[182] 3.054s passed
getAnyOfNPermInv data()[183] 3.077s passed
seqNPermRange data()[184] 3.121s passed
seqPermTrans data()[185] 3.090s passed
seqPermRefl data()[186] 3.090s passed
seqPermSplit data()[187] 3.056s passed
seqNPermRight data()[188] 3.266s passed
seqPermFromSwap data()[189] 3.165s passed
divResZero1 data()[18] 3.109s passed
seqPermTransAlt0 data()[190] 3.106s passed
seqPermTransAlt1 data()[191] 3.172s passed
seqPermTransAlt2 data()[192] 3.142s passed
seqPermTransAlt3 data()[193] 3.123s passed
seqPermForall data()[194] 3.165s passed
seqPermExists data()[195] 3.132s passed
schiffl_lemma_2 data()[196] 21.173s passed
schiffl_thm_1 data()[197] 3.896s passed
eqSameSeq data()[198] 3.191s passed
divResZero2 data()[19] 3.100s passed
eqTermCut data()[1] 3.745s passed
divResOne1 data()[20] 3.127s passed
divResOne2 data()[21] 3.094s passed
div_cancel1 data()[22] 3.091s passed
div_cancel2 data()[23] 3.085s passed
divAddMultDenom data()[24] 3.135s passed
divMinus data()[25] 3.158s passed
divMinusDenom data()[26] 3.119s passed
divLeastDPos data()[27] 3.082s passed
divLeastDNeg data()[28] 3.080s passed
divGreatestDPos data()[29] 3.085s passed
equivAllRight data()[2] 3.408s passed
divGreatestDNeg data()[30] 3.082s passed
divIncreasingPos data()[31] 3.073s passed
divIncreasingNeg data()[32] 3.114s passed
jdiv_zero data()[33] 3.092s passed
jdivPulloutMinusNum data()[34] 3.074s passed
jdivPulloutMinusDenom data()[35] 3.129s passed
jdiv_uniquePosPos data()[36] 3.082s passed
jdiv_uniquePosNeg data()[37] 3.085s passed
jdiv_uniqueNegPos data()[38] 3.094s passed
jdiv_uniqueNegNeg data()[39] 3.076s passed
irrflConcrete1 data()[3] 3.306s passed
jdivMultDenom1 data()[40] 3.087s passed
jdivMultDenom2 data()[41] 3.143s passed
mod_geZero data()[42] 3.065s passed
mod_lessDenom data()[43] 3.057s passed
jmod_NumPos data()[44] 3.074s passed
jmod_NumNeg data()[45] 3.111s passed
jmod_geZero data()[46] 3.072s passed
jmodNumZero data()[47] 3.056s passed
jmod_pulloutminusNum data()[48] 3.097s passed
jmod_pulloutminusDenom data()[49] 3.057s passed
irrflConcrete2 data()[4] 3.278s passed
jmodUnique1 data()[50] 3.116s passed
jmodUnique2 data()[51] 3.168s passed
intDivRem data()[52] 3.134s passed
jmodjmod data()[53] 3.069s passed
jmodDivisible data()[54] 3.091s passed
jmodDivisibleRep data()[55] 3.051s passed
jdivAddMultDenom data()[56] 3.218s passed
jmodAltZero data()[57] 3.063s passed
jmodAddMultDenomZero data()[58] 3.049s passed
polyDiv_zero data()[59] 3.048s passed
cancel_gtPos data()[5] 3.324s passed
polyMod_ltdivDenom data()[60] 3.079s passed
bsum_empty data()[61] 3.028s passed
bsum_induction_upper data()[62] 3.039s passed
bsum_induction_lower data()[63] 3.078s passed
bsum_num_of_bounds data()[64] 3.080s passed
bsum_num_of_bounds2 data()[65] 3.065s passed
bsum_induction_upper2 data()[66] 3.063s passed
bsum_induction_upper_concrete data()[67] 3.059s passed
bsum_induction_upper_concrete_2 data()[68] 3.041s passed
bsum_induction_upper2_concrete data()[69] 3.065s passed
cancel_gtNeg data()[6] 3.281s passed
bsum_induction_lower_concrete data()[70] 3.053s passed
bsum_induction_lower2 data()[71] 3.052s passed
bsum_induction_lower2_concrete data()[72] 3.072s passed
bsum_positive data()[73] 3.110s passed
bsum_upper_bound data()[74] 3.086s passed
bsum_lower_bound data()[75] 3.094s passed
bsum_positive_lower_bound_element data()[76] 3.090s passed
bsum_sub_same_index data()[77] 3.070s passed
bsum_less_same_index data()[78] 3.125s passed
bsum_equal_except_one_index data()[79] 3.069s passed
moduloIntIsInInt data()[7] 3.209s passed
bsum_num_of_is_max data()[80] 3.064s passed
bsum_num_of_is_max2 data()[81] 3.093s passed
bsum_num_of_is_max3 data()[82] 3.070s passed
bsum_num_of_is_max4 data()[83] 3.068s passed
bsum_num_of_lt_max data()[84] 3.124s passed
bsum_num_of_lt_max2 data()[85] 3.072s passed
bsum_num_of_lt_max3 data()[86] 3.065s passed
bsum_num_of_lt_max4 data()[87] 3.080s passed
bsum_num_of_gt0 data()[88] 3.074s passed
bsum_num_of_gt0_alt data()[89] 3.052s passed
moduloLongIsInLong data()[8] 3.200s passed
bsum_add_concrete data()[90] 3.068s passed
bprod_all_positive data()[91] 3.058s passed
bprod_split data()[92] 3.035s passed
powConcrete0 data()[93] 3.064s passed
powConcrete1 data()[94] 3.039s passed
powSplitFactor data()[95] 3.059s passed
powAdd data()[96] 3.079s passed
powMono data()[97] 3.054s passed
powMonoConcrete data()[98] 3.036s passed
powMonoConcreteRight data()[99] 3.039s passed
moduloShortIsInShort data()[9] 3.123s passed

Standard output

335        INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src/test/resources/testcase/dummyTrue.key 
356        DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 8.83ms 
547        INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
566        WARN  Test worker     d.u.i.k.s.ProofSettings   The settings in /home/runner/.key/proof-settings.props are *not* read. 
1384       DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for Meta 
1388       DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for Meta 
1391       DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for Meta 
1391       DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for Meta 
2699       DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for JavaBigintExpression 
7747       DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 7.2s 
7806       INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof dummyTrue.key 
7836       DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 30.7ns 
7848       INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/firstOrder/Taclet_eqTermCut.proof 
7848       DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 159.3ns 
7851       INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
10583      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.73s 
10585      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: eqTermCut 
11563      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: eqTermCut 
11585      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 16.84ms 
11594      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/firstOrder/Taclet_equivAllRight.proof 
11594      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 212.3ns 
11596      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
14125      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.53s 
14125      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: equivAllRight 
14986      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: equivAllRight 
15000      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 10.48ms 
15004      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_irrflConcrete1.proof 
15004      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 130.8ns 
15005      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
17479      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.47s 
17480      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: irrflConcrete1 
18300      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: irrflConcrete1 
18306      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.18ms 
18309      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_irrflConcrete2.proof 
18310      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 321.3ns 
18311      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
20777      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.47s 
20777      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: irrflConcrete2 
21580      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: irrflConcrete2 
21585      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.79ms 
21588      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_cancel_gtPos.proof 
21588      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 327.1ns 
21590      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
23996      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.41s 
23997      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: cancel_gtPos 
24828      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: cancel_gtPos 
24906      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 68.86ms 
24914      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_cancel_gtNeg.proof 
24914      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 136.5ns 
24915      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
27324      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.41s 
27324      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: cancel_gtNeg 
28157      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: cancel_gtNeg 
28194      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 33.17ms 
28197      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intRulesIgnoringOF/Taclet_moduloIntIsInInt.proof 
28198      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 585.9ns 
28199      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
30620      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.42s 
30620      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: moduloIntIsInInt 
31401      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: moduloIntIsInInt 
31404      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 496.7ns 
31407      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intRulesIgnoringOF/Taclet_moduloLongIsInLong.proof 
31407      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 318.4ns 
31408      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
33771      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.36s 
33772      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: moduloLongIsInLong 
34602      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: moduloLongIsInLong 
34605      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 533.4ns 
34606      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intRulesIgnoringOF/Taclet_moduloShortIsInShort.proof 
34606      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 114.8ns 
34607      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
36944      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.34s 
36944      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: moduloShortIsInShort 
37723      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: moduloShortIsInShort 
37727      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 506.2ns 
37729      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intRulesIgnoringOF/Taclet_moduloByteIsInByte.proof 
37730      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 335.9ns 
37731      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
40078      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.35s 
40078      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: moduloByteIsInByte 
40850      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: moduloByteIsInByte 
40853      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 559.7ns 
40855      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intRulesIgnoringOF/Taclet_moduloCharIsInChar.proof 
40855      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 308.9ns 
40856      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
43187      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.33s 
43188      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: moduloCharIsInChar 
43966      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: moduloCharIsInChar 
43969      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 537.4ns 
43971      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_div_unique1.proof 
43971      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 320.4ns 
43972      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
46291      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.32s 
46291      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: div_unique1 
47059      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: div_unique1 
47115      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 51.89ms 
47121      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_div_unique2.proof 
47122      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 124.8ns 
47122      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
49525      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.4s 
49525      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: div_unique2 
50267      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: div_unique2 
50300      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 29.84ms 
50302      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_div_exists.proof 
50302      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 127.3ns 
50303      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
52647      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.34s 
52647      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: div_exists 
53409      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: div_exists 
53563      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 144.69ms 
53566      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_div_one.proof 
53566      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 233.3ns 
53567      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
55889      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.32s 
55890      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: div_one 
56654      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: div_one 
56659      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.66ms 
56660      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdiv_one.proof 
56660      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 108.4ns 
56661      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
59009      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.35s 
59010      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdiv_one 
59776      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdiv_one 
59779      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.13ms 
59782      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_div_zero.proof 
59782      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 308.8ns 
59783      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
62124      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.34s 
62124      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: div_zero 
62900      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: div_zero 
62938      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 33.26ms 
62940      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divResZero1.proof 
62941      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 343.4ns 
62942      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
65252      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.31s 
65252      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divResZero1 
66020      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divResZero1 
66047      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 17.01ms 
66049      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divResZero2.proof 
66049      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 104.5ns 
66049      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
68382      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.33s 
68382      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divResZero2 
69128      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divResZero2 
69147      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 15.49ms 
69149      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divResOne1.proof 
69149      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 286ns 
69154      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
71501      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.35s 
71501      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divResOne1 
72259      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divResOne1 
72274      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 12.6ms 
72276      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divResOne2.proof 
72276      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 95.4ns 
72277      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
74593      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.32s 
74593      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divResOne2 
75355      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divResOne2 
75368      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 11.08ms 
75370      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_div_cancel1.proof 
75370      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 125.6ns 
75371      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
77697      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.33s 
77697      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: div_cancel1 
78435      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: div_cancel1 
78459      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 20.21ms 
78460      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_div_cancel2.proof 
78460      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 106.4ns 
78461      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
80784      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.32s 
80784      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: div_cancel2 
81541      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: div_cancel2 
81544      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.01ms 
81545      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divAddMultDenom.proof 
81545      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 81.1ns 
81546      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
83877      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.33s 
83877      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divAddMultDenom 
84641      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divAddMultDenom 
84680      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 33.9ms 
84681      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divMinus.proof 
84681      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 100.2ns 
84682      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
87028      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.35s 
87028      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divMinus 
87774      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divMinus 
87837      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 52.01ms 
87840      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divMinusDenom.proof 
87840      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 347.9ns 
87841      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
90159      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.32s 
90159      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divMinusDenom 
90916      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divMinusDenom 
90957      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 36.14ms 
90959      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divLeastDPos.proof 
90959      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 106.4ns 
90960      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
93274      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.31s 
93274      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divLeastDPos 
94033      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divLeastDPos 
94039      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.91ms 
94041      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divLeastDNeg.proof 
94041      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 75.1ns 
94041      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
96369      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.33s 
96369      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divLeastDNeg 
97107      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divLeastDNeg 
97119      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 9.63ms 
97120      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divGreatestDPos.proof 
97120      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 85.6ns 
97121      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
99438      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.32s 
99438      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divGreatestDPos 
100194     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divGreatestDPos 
100204     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 8.22ms 
100205     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divGreatestDNeg.proof 
100205     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 81.3ns 
100206     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
102525     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.32s 
102526     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divGreatestDNeg 
103279     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divGreatestDNeg 
103286     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 5.3ms 
103288     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divIncreasingPos.proof 
103288     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 93.1ns 
103288     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
105609     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.32s 
105609     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divIncreasingPos 
106346     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divIncreasingPos 
106359     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 11.15ms 
106362     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divIncreasingNeg.proof 
106364     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 2.08ms 
106365     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
108709     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.34s 
108710     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divIncreasingNeg 
109466     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divIncreasingNeg 
109473     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.83ms 
109474     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdiv_zero.proof 
109474     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 94.1ns 
109475     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
111780     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.3s 
111780     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdiv_zero 
112560     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdiv_zero 
112565     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.62ms 
112567     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdivPulloutMinusNum.proof 
112567     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 663.2ns 
112568     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
114891     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.32s 
114892     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdivPulloutMinusNum 
115626     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdivPulloutMinusNum 
115637     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 7.98ms 
115641     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdivPulloutMinusDenom.proof 
115641     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 101.9ns 
115642     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
117964     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.32s 
117965     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdivPulloutMinusDenom 
118718     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdivPulloutMinusDenom 
118768     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 44.05ms 
118771     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdiv_uniquePosPos.proof 
118771     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 298.1ns 
118772     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
121078     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.31s 
121079     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdiv_uniquePosPos 
121833     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdiv_uniquePosPos 
121850     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 13.54ms 
121853     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdiv_uniquePosNeg.proof 
121853     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 273.5ns 
121854     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
124159     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.3s 
124159     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdiv_uniquePosNeg 
124919     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdiv_uniquePosNeg 
124936     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 14.23ms 
124937     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdiv_uniqueNegPos.proof 
124937     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 103.2ns 
124938     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
127254     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.32s 
127254     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdiv_uniqueNegPos 
128010     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdiv_uniqueNegPos 
128030     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 17.37ms 
128031     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdiv_uniqueNegNeg.proof 
128032     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 77.5ns 
128032     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
130337     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.3s 
130337     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdiv_uniqueNegNeg 
131091     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdiv_uniqueNegNeg 
131106     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 13.05ms 
131108     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdivMultDenom1.proof 
131108     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 83.5ns 
131109     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
133400     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.29s 
133400     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdivMultDenom1 
134155     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdivMultDenom1 
134193     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 33.96ms 
134195     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdivMultDenom2.proof 
134195     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 78.3ns 
134195     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
136575     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.38s 
136576     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdivMultDenom2 
137334     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdivMultDenom2 
137337     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.45ms 
137338     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_mod_geZero.proof 
137338     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 70.9ns 
137339     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
139641     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.3s 
139641     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: mod_geZero 
140397     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: mod_geZero 
140401     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.33ms 
140402     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_mod_lessDenom.proof 
140402     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 63.5ns 
140403     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
142697     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.29s 
142697     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: mod_lessDenom 
143451     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: mod_lessDenom 
143458     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 5.27ms 
143460     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmod_NumPos.proof 
143460     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 77.6ns 
143461     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
145768     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.31s 
145768     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmod_NumPos 
146520     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmod_NumPos 
146532     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 9.89ms 
146534     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmod_NumNeg.proof 
146534     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 265.8ns 
146535     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
148873     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.34s 
148873     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmod_NumNeg 
149626     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmod_NumNeg 
149644     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 14.62ms 
149645     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmod_geZero.proof 
149645     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 73.6ns 
149646     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
151953     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.31s 
151953     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmod_geZero 
152707     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmod_geZero 
152715     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 6.16ms 
152717     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmodNumZero.proof 
152717     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 80.7ns 
152717     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
155032     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.31s 
155032     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmodNumZero 
155768     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmodNumZero 
155771     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.29ms 
155773     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmod_pulloutminusNum.proof 
155773     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 239.2ns 
155779     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
158108     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.33s 
158108     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmod_pulloutminusNum 
158865     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmod_pulloutminusNum 
158868     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.78ms 
158870     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmod_pulloutminusDenom.proof 
158870     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 68ns 
158870     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
161169     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.3s 
161169     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmod_pulloutminusDenom 
161921     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmod_pulloutminusDenom 
161925     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.35ms 
161926     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmodUnique1.proof 
161927     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 75.7ns 
161927     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
164243     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.32s 
164243     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmodUnique1 
164976     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmodUnique1 
165042     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 57.43ms 
165043     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmodUnique2.proof 
165043     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 77.5ns 
165044     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
167374     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.33s 
167374     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmodUnique2 
168132     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmodUnique2 
168210     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 69.61ms 
168211     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_intDivRem.proof 
168211     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 151.4ns 
168212     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
170585     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.37s 
170585     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: intDivRem 
171340     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: intDivRem 
171344     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.89ms 
171345     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmodjmod.proof 
171345     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 73.5ns 
171346     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
173650     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.3s 
173650     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmodjmod 
174381     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmodjmod 
174412     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 28.39ms 
174414     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmodDivisible.proof 
174414     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 180.1ns 
174414     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
176724     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.31s 
176724     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmodDivisible 
177476     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmodDivisible 
177503     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 23.32ms 
177505     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmodDivisibleRep.proof 
177505     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 238.7ns 
177506     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
179796     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.29s 
179796     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmodDivisibleRep 
180551     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmodDivisibleRep 
180554     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 950.4ns 
180556     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdivAddMultDenom.proof 
180556     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 76.8ns 
180557     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
182865     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.31s 
182865     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdivAddMultDenom 
183598     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdivAddMultDenom 
183772     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 163.19ms 
183773     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmodAltZero.proof 
183774     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 82.7ns 
183774     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
186067     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.29s 
186067     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmodAltZero 
186822     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmodAltZero 
186835     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 11.55ms 
186837     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmodAddMultDenomZero.proof 
186837     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 71.9ns 
186839     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
189128     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.29s 
189128     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmodAddMultDenomZero 
189877     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmodAddMultDenomZero 
189884     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 5.35ms 
189885     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_polyDiv_zero.proof 
189885     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 72.2ns 
189886     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
192186     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.3s 
192187     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: polyDiv_zero 
192917     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: polyDiv_zero 
192932     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 12.45ms 
192933     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_polyMod_ltdivDenom.proof 
192933     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 82.9ns 
192934     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
195248     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.31s 
195248     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: polyMod_ltdivDenom 
195998     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: polyMod_ltdivDenom 
196010     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 6.31ms 
196012     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_empty.proof 
196012     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 74.9ns 
196013     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
198289     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.28s 
198289     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_empty 
199036     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_empty 
199039     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.46ms 
199041     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_induction_upper.proof 
199041     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 206.8ns 
199042     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
201342     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.3s 
201342     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_upper 
202074     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_induction_upper 
202078     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.98ms 
202079     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_induction_lower.proof 
202080     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 69ns 
202080     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
204381     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.3s 
204382     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_lower 
205131     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_induction_lower 
205156     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 22.53ms 
205159     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_bounds.proof 
205159     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 273.8ns 
205160     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
207465     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.3s 
207465     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_bounds 
208221     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_bounds 
208237     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 12.5ms 
208238     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_bounds2.proof 
208238     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 94.5ns 
208239     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
210556     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.32s 
210556     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_bounds2 
211287     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_bounds2 
211302     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 12.04ms 
211303     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_induction_upper2.proof 
211303     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 67.8ns 
211304     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
213610     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.31s 
213610     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_upper2 
214360     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_induction_upper2 
214364     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.58ms 
214366     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_induction_upper_concrete.proof 
214366     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 217.5ns 
214367     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
216668     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.3s 
216668     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_upper_concrete 
217419     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_induction_upper_concrete 
217423     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.56ms 
217424     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_induction_upper_concrete_2.proof 
217424     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 58.5ns 
217425     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
219728     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.3s 
219728     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_upper_concrete_2 
220459     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_induction_upper_concrete_2 
220464     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.3ms 
220465     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_induction_upper2_concrete.proof 
220466     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 65.9ns 
220466     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
222779     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.31s 
222779     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_upper2_concrete 
223527     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_induction_upper2_concrete 
223530     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.33ms 
223531     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_induction_lower_concrete.proof 
223531     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 69.2ns 
223532     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
225822     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.29s 
225822     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_lower_concrete 
226580     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_induction_lower_concrete 
226582     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 649.2ns 
226583     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_induction_lower2.proof 
226583     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 60.4ns 
226584     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
228900     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.32s 
228900     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_lower2 
229631     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_induction_lower2 
229634     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.12ms 
229635     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_induction_lower2_concrete.proof 
229636     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 72.3ns 
229636     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
231948     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.31s 
231948     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_lower2_concrete 
232704     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_induction_lower2_concrete 
232706     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 959.9ns 
232708     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_positive.proof 
232708     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 155.4ns 
232709     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
234998     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.29s 
234998     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_positive 
235751     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_positive 
235816     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 62.75ms 
235818     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_upper_bound.proof 
235818     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 83.3ns 
235819     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
238119     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.3s 
238119     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_upper_bound 
238869     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_upper_bound 
238902     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 30.14ms 
238903     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_lower_bound.proof 
238903     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 65ns 
238904     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
241214     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.31s 
241214     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_lower_bound 
241964     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_lower_bound 
241996     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 28.65ms 
241999     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_positive_lower_bound_element.proof 
241999     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 84.3ns 
242000     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
244293     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.29s 
244293     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_positive_lower_bound_element 
245045     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_positive_lower_bound_element 
245087     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 38.61ms 
245089     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_sub_same_index.proof 
245089     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 196.5ns 
245090     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
247378     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.29s 
247378     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_sub_same_index 
248130     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_sub_same_index 
248158     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 24.97ms 
248159     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_less_same_index.proof 
248159     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 73.4ns 
248160     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
250474     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.31s 
250474     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_less_same_index 
251233     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_less_same_index 
251282     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 44.14ms 
251283     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_equal_except_one_index.proof 
251284     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 76.3ns 
251284     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
253576     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.29s 
253577     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_equal_except_one_index 
254326     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_equal_except_one_index 
254351     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 22.7ms 
254353     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_is_max.proof 
254353     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 80.1ns 
254353     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
256646     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.29s 
256666     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_is_max 
257397     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_is_max 
257415     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 15.64ms 
257416     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_is_max2.proof 
257416     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 67.6ns 
257417     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
259733     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.32s 
259733     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_is_max2 
260483     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_is_max2 
260508     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 21.94ms 
260510     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_is_max3.proof 
260510     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 87.1ns 
260510     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
262810     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.3s 
262810     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_is_max3 
263560     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_is_max3 
263578     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 15.84ms 
263579     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_is_max4.proof 
263579     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 69.4ns 
263580     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
265870     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.29s 
265871     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_is_max4 
266620     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_is_max4 
266647     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 23.71ms 
266648     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_lt_max.proof 
266648     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 78ns 
266649     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
268990     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.34s 
268990     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_lt_max 
269741     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_lt_max 
269770     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 26.08ms 
269772     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_lt_max2.proof 
269772     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 203.9ns 
269773     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
272066     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.29s 
272067     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_lt_max2 
272819     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_lt_max2 
272843     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 20.55ms 
272844     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_lt_max3.proof 
272844     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 74.4ns 
272845     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
275129     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.28s 
275129     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_lt_max3 
275884     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_lt_max3 
275908     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 20.95ms 
275909     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_lt_max4.proof 
275909     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 81.7ns 
275910     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
278213     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.3s 
278213     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_lt_max4 
278963     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_lt_max4 
278987     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 21.26ms 
278989     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_gt0.proof 
278989     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 196.8ns 
278990     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
281281     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.29s 
281281     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_gt0 
282033     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_gt0 
282061     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 25.21ms 
282062     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_gt0_alt.proof 
282062     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 68.5ns 
282063     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
284341     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.28s 
284342     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_gt0_alt 
285090     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_gt0_alt 
285114     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 21.31ms 
285115     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_add_concrete.proof 
285115     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 67.7ns 
285115     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
287419     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.3s 
287419     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_add_concrete 
288173     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_add_concrete 
288181     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 6.64ms 
288183     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bprod/Taclet_bprod_all_positive.proof 
288183     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 163.3ns 
288184     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
290472     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.29s 
290472     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bprod_all_positive 
291222     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bprod_all_positive 
291239     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 14.2ms 
291240     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bprod/Taclet_bprod_split.proof 
291240     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 48.9ns 
291241     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
293520     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.28s 
293520     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bprod_split 
294271     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bprod_split 
294275     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.86ms 
294276     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powConcrete0.proof 
294276     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 50.4ns 
294276     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
296583     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.31s 
296584     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powConcrete0 
297336     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powConcrete0 
297338     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 552.6ns 
297339     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powConcrete1.proof 
297339     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 54.6ns 
297340     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
299625     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.29s 
299625     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powConcrete1 
300375     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powConcrete1 
300377     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 691.9ns 
300378     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powSplitFactor.proof 
300378     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 48.4ns 
300379     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
302672     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.29s 
302672     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powSplitFactor 
303423     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powSplitFactor 
303435     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 10.18ms 
303439     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powAdd.proof 
303439     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 231.4ns 
303440     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
305751     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.31s 
305752     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powAdd 
306509     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powAdd 
306516     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.99ms 
306518     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powMono.proof 
306518     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 193.6ns 
306519     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
308807     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.29s 
308807     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powMono 
309559     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powMono 
309571     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 9.25ms 
309572     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powMonoConcrete.proof 
309572     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 56.1ns 
309573     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
311854     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.28s 
311854     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powMonoConcrete 
312603     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powMonoConcrete 
312606     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.78ms 
312607     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powMonoConcreteRight.proof 
312607     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 46.4ns 
312608     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
314913     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.31s 
314913     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powMonoConcreteRight 
315644     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powMonoConcreteRight 
315646     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 548.6ns 
315647     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powPositive.proof 
315647     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 53.8ns 
315648     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
317956     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.31s 
317956     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powPositive 
318705     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powPositive 
318710     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.38ms 
318711     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powPositiveConcrete.proof 
318711     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 48.6ns 
318712     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
320990     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.28s 
320990     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powPositiveConcrete 
321739     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powPositiveConcrete 
321741     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 609.9ns 
321742     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powGeq1Concrete.proof 
321742     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 45.5ns 
321743     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
324039     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.3s 
324039     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powGeq1Concrete 
324770     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powGeq1Concrete 
324772     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 535.7ns 
324773     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_pow2InIntLower.proof 
324773     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 47.9ns 
324773     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
327078     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.3s 
327078     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: pow2InIntLower 
327829     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: pow2InIntLower 
327831     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 558.6ns 
327833     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_pow2InIntUpper.proof 
327833     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 161.6ns 
327834     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
330119     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.28s 
330119     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: pow2InIntUpper 
330870     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: pow2InIntUpper 
330873     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.8ms 
330874     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logSelfConcrete.proof 
330874     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 45.9ns 
330875     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
333176     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.3s 
333176     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logSelfConcrete 
333911     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logSelfConcrete 
333919     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 6.46ms 
333920     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_log1Concrete.proof 
333920     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 54.4ns 
333921     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
336246     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.33s 
336247     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: log1Concrete 
336999     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: log1Concrete 
337002     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.17ms 
337003     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logProduct.proof 
337003     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 56.2ns 
337004     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
339296     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.29s 
339297     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logProduct 
340048     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logProduct 
340055     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.68ms 
340057     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logTimesBaseConcrete.proof 
340057     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 160.2ns 
340058     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
342362     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.3s 
342362     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logTimesBaseConcrete 
343093     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logTimesBaseConcrete 
343097     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.08ms 
343098     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logProdIdentity.proof 
343098     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 62.9ns 
343099     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
345395     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.3s 
345395     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logProdIdentity 
346144     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logProdIdentity 
346159     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 12.12ms 
346160     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logProdIdentityConcrete.proof 
346160     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 63.1ns 
346160     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
348450     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.29s 
348450     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logProdIdentityConcrete 
349199     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logProdIdentityConcrete 
349202     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.62ms 
349203     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logPowIdentity.proof 
349203     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 54.5ns 
349204     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
351500     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.3s 
351500     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logPowIdentity 
352230     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logPowIdentity 
352235     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.59ms 
352237     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logPowIdentityConcrete.proof 
352237     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 175.5ns 
352238     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
354537     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.3s 
354538     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logPowIdentityConcrete 
355287     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logPowIdentityConcrete 
355291     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.96ms 
355292     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logPositive.proof 
355292     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 46.3ns 
355293     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
357571     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.28s 
357572     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logPositive 
358323     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logPositive 
358340     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 14.62ms 
358342     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logPositiveConcrete.proof 
358342     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 201.2ns 
358343     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
360654     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.31s 
360654     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logPositiveConcrete 
361385     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logPositiveConcrete 
361389     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 638.6ns 
361391     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logMono.proof 
361391     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 52.9ns 
361391     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
363681     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.29s 
363681     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logMono 
364428     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logMono 
364466     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 33.47ms 
364467     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logMonoConcrete.proof 
364467     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 58.7ns 
364468     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
366747     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.28s 
366748     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logMonoConcrete 
367498     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logMonoConcrete 
367501     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.68ms 
367502     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powLogLess.proof 
367502     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 48.2ns 
367503     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
369802     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.3s 
369802     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powLogLess 
370556     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powLogLess 
370577     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 18.53ms 
370579     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powLogMore2.proof 
370579     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 67.5ns 
370580     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
372863     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.28s 
372863     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powLogMore2 
373613     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powLogMore2 
373633     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 17.48ms 
373634     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logLessThanPow.proof 
373634     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 61.5ns 
373635     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
375941     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.31s 
375941     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logLessThanPow 
376689     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logLessThanPow 
376712     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 20.25ms 
376713     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logLessThanPowConcrete.proof 
376713     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 61.7ns 
376714     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
378995     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.28s 
378995     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logLessThanPowConcrete 
379748     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logLessThanPowConcrete 
379751     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 659.4ns 
379754     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logSqueeze.proof 
379754     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 187.8ns 
379755     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
382056     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.3s 
382056     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logSqueeze 
382787     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logSqueeze 
382792     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.64ms 
382793     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/booleanRules/Taclet_ifthenelse_equals.proof 
382793     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 48ns 
382794     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
385093     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.3s 
385093     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: ifthenelse_equals 
385848     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: ifthenelse_equals 
385852     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.26ms 
385854     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/booleanRules/Taclet_ifthenelse_equals_1.proof 
385854     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 176.9ns 
385855     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
388155     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.3s 
388155     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: ifthenelse_equals_1 
388889     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: ifthenelse_equals_1 
388892     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 743.9ns 
388893     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/booleanRules/Taclet_ifthenelse_equals_2.proof 
388893     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 45.3ns 
388894     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
391190     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.3s 
391190     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: ifthenelse_equals_2 
391942     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: ifthenelse_equals_2 
391944     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 761.5ns 
391945     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/locSet/Taclet_disjointWithSingleton1.proof 
391945     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 46.2ns 
391946     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
394244     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.3s 
394244     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: disjointWithSingleton1 
394980     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: disjointWithSingleton1 
394983     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.4ms 
394985     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/locSet/Taclet_disjointWithSingleton2.proof 
394985     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 45ns 
394985     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
397285     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.3s 
397285     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: disjointWithSingleton2 
398038     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: disjointWithSingleton2 
398042     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.77ms 
398043     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/locSet/Taclet_disjointArrayRanges.proof 
398044     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 57ns 
398044     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
400344     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.3s 
400344     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: disjointArrayRanges 
401079     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: disjointArrayRanges 
401088     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 7.03ms 
401089     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/locSet/Taclet_disjointArrayRangeAllFields1.proof 
401089     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 52.4ns 
401090     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
403409     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.32s 
403409     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: disjointArrayRangeAllFields1 
404164     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: disjointArrayRangeAllFields1 
404176     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 9.73ms 
404177     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/locSet/Taclet_disjointArrayRangeAllFields2.proof 
404177     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 53ns 
404177     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
406478     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.3s 
406478     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: disjointArrayRangeAllFields2 
407214     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: disjointArrayRangeAllFields2 
407224     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 8.61ms 
407225     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqSelfDefinition.proof 
407225     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 59.6ns 
407226     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
409521     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.3s 
409521     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqSelfDefinition 
410278     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqSelfDefinition 
410290     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 10.12ms 
410292     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqOutsideValue.proof 
410292     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 59.4ns 
410292     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
412593     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.3s 
412593     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqOutsideValue 
413357     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqOutsideValue 
413362     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.24ms 
413364     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_castedGetAny.proof 
413364     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 158.6ns 
413365     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
415650     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.28s 
415650     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: castedGetAny 
416409     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: castedGetAny 
416416     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 5.89ms 
416418     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqGetAlphaCast.proof 
416418     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 163.1ns 
416419     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
418727     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.31s 
418727     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqGetAlphaCast 
419486     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqGetAlphaCast 
419488     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 549.6ns 
419489     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqSingleton.proof 
419489     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 54.9ns 
419490     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
421789     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.3s 
421789     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqSingleton 
422528     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqSingleton 
422530     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.18ms 
422531     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqSingletonConcrete.proof 
422531     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 50.3ns 
422532     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
424826     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.29s 
424826     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqSingletonConcrete 
425582     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqSingletonConcrete 
425584     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 717.6ns 
425585     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqConcat.proof 
425586     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 55.5ns 
425586     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
427883     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.3s 
427883     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqConcat 
428641     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqConcat 
428651     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 8.33ms 
428653     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqSub.proof 
428653     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 55.4ns 
428653     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
430955     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.3s 
430955     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqSub 
431716     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqSub 
431720     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.38ms 
431721     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqReverse.proof 
431721     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 136ns 
431722     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
434024     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.3s 
434024     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqReverse 
434787     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqReverse 
434793     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.69ms 
434795     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqEmpty.proof 
434795     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 61.7ns 
434795     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
437115     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.32s 
437115     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqEmpty 
437874     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqEmpty 
437876     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 674ns 
437877     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqSingleton.proof 
437877     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 55.8ns 
437878     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
440170     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.29s 
440170     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqSingleton 
440928     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqSingleton 
440930     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 618.6ns 
440931     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqConcat.proof 
440931     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 55.9ns 
440932     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
443233     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.3s 
443233     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqConcat 
443993     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqConcat 
443997     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.05ms 
443998     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqSub.proof 
443998     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 48.8ns 
443998     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
446298     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.3s 
446298     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqSub 
447055     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqSub 
447057     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.25ms 
447058     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqReverse.proof 
447059     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 54.6ns 
447059     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
449345     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.29s 
449346     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqReverse 
450103     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqReverse 
450106     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.37ms 
450107     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_equalityToSeqGetAndSeqLenLeft.proof 
450107     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 45.6ns 
450107     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
452405     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.3s 
452406     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: equalityToSeqGetAndSeqLenLeft 
453179     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: equalityToSeqGetAndSeqLenLeft 
453182     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.21ms 
453183     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_equalityToSeqGetAndSeqLenRight.proof 
453183     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 52.9ns 
453183     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
455561     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.38s 
455561     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: equalityToSeqGetAndSeqLenRight 
456337     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: equalityToSeqGetAndSeqLenRight 
456342     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.43ms 
456343     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqSingletonEQ.proof 
456343     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 45.9ns 
456344     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
458641     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.3s 
458641     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqSingletonEQ 
459380     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqSingletonEQ 
459383     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.39ms 
459384     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqConcatEQ.proof 
459384     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 54.9ns 
459384     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
461681     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.3s 
461681     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqConcatEQ 
462441     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqConcatEQ 
462452     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 8.38ms 
462453     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqSubEQ.proof 
462453     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 58ns 
462453     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
464748     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.29s 
464748     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqSubEQ 
465507     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqSubEQ 
465509     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 630.3ns 
465510     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqReverseEQ.proof 
465510     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 53.1ns 
465510     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
467817     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.31s 
467817     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqReverseEQ 
468581     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqReverseEQ 
468587     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.73ms 
468589     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqEmptyEQ.proof 
468589     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 54.3ns 
468589     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
470896     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.31s 
470896     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqEmptyEQ 
471655     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqEmptyEQ 
471657     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 777.7ns 
471658     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqSingletonEQ.proof 
471658     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 50.2ns 
471659     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
473937     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.28s 
473937     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqSingletonEQ 
474693     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqSingletonEQ 
474695     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 756.3ns 
474696     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqConcatEQ.proof 
474697     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 54.1ns 
474697     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
476992     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.3s 
476992     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqConcatEQ 
477749     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqConcatEQ 
477754     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.07ms 
477755     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqSubEQ.proof 
477755     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 54.9ns 
477756     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
480051     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.3s 
480051     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqSubEQ 
480809     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqSubEQ 
480812     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.55ms 
480813     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqReverseEQ.proof 
480813     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 56.9ns 
480813     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
483108     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.29s 
483108     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqReverseEQ 
483866     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqReverseEQ 
483869     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.63ms 
483872     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqDefEQ.proof 
483872     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 70.8ns 
483873     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
486169     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.3s 
486169     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqDefEQ 
486928     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqDefEQ 
486931     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.99ms 
486934     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqDefEQ.proof 
486934     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 55.7ns 
486934     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
489232     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.3s 
489232     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqDefEQ 
489990     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqDefEQ 
489995     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.95ms 
489996     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqConcatWithSeqEmpty1.proof 
489996     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 54.5ns 
489996     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
492302     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.31s 
492302     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqConcatWithSeqEmpty1 
493044     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqConcatWithSeqEmpty1 
493058     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 11.82ms 
493059     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqConcatWithSeqEmpty2.proof 
493059     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 57.9ns 
493060     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
495367     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.31s 
495367     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqConcatWithSeqEmpty2 
496126     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqConcatWithSeqEmpty2 
496141     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 12.84ms 
496142     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqReverseOfSeqEmpty.proof 
496142     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 57.8ns 
496143     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
498444     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.3s 
498444     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqReverseOfSeqEmpty 
499202     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqReverseOfSeqEmpty 
499212     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 8.1ms 
499213     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_subSeqComplete.proof 
499213     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 55ns 
499214     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
501520     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.31s 
501520     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: subSeqComplete 
502282     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: subSeqComplete 
502293     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 8.48ms 
502294     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_subSeqTailR.proof 
502294     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 56.7ns 
502294     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
504592     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.3s 
504593     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: subSeqTailR 
505350     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: subSeqTailR 
505374     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 22.03ms 
505375     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_subSeqTailL.proof 
505375     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 52.6ns 
505376     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
507672     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.3s 
507672     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: subSeqTailL 
508431     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: subSeqTailL 
508454     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 21.8ms 
508456     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_subSeqTailEQR.proof 
508456     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 61.3ns 
508456     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
510753     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.3s 
510753     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: subSeqTailEQR 
511512     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: subSeqTailEQR 
511535     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 20.45ms 
511536     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_subSeqTailEQL.proof 
511536     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 50.2ns 
511536     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
513835     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.3s 
513835     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: subSeqTailEQL 
514593     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: subSeqTailEQL 
514606     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 11.61ms 
514607     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDef_split.proof 
514607     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 59ns 
514608     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
516912     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.3s 
516912     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_split 
517677     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDef_split 
517706     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 26.03ms 
517708     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDef_induction_upper.proof 
517708     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 59.6ns 
517708     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
520026     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.32s 
520026     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_induction_upper 
520790     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDef_induction_upper 
520846     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 53.54ms 
520848     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDef_induction_upper_concrete.proof 
520848     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 64ns 
520848     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
523155     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.31s 
523155     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_induction_upper_concrete 
523914     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDef_induction_upper_concrete 
523952     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 35.01ms 
523954     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDef_induction_lower.proof 
523954     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 212.4ns 
523955     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
526254     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.3s 
526254     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_induction_lower 
527015     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDef_induction_lower 
527055     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 37.69ms 
527056     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDef_induction_lower_concrete.proof 
527056     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 61.3ns 
527057     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
529363     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.31s 
529363     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_induction_lower_concrete 
530123     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDef_induction_lower_concrete 
530166     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 39.76ms 
530167     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDef_split_in_three.proof 
530167     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 62.4ns 
530168     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
532469     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.3s 
532469     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_split_in_three 
533228     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDef_split_in_three 
533342     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 107.31ms 
533343     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDef_empty.proof 
533344     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 62.7ns 
533344     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
535668     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.32s 
535668     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_empty 
536433     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDef_empty 
536441     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 5.8ms 
536442     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDef_one_summand.proof 
536442     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 55.4ns 
536442     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
538749     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.31s 
538749     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_one_summand 
539510     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDef_one_summand 
539517     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 5.54ms 
539518     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDef_lower_equals_upper.proof 
539518     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 55.9ns 
539519     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
541820     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.3s 
541820     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_lower_equals_upper 
542579     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDef_lower_equals_upper 
542584     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.43ms 
542585     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDefOfSeq.proof 
542585     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 54ns 
542586     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
544884     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.3s 
544884     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDefOfSeq 
545642     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDefOfSeq 
545659     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 14.12ms 
545660     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqSelfDefinitionEQ2.proof 
545660     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 52.9ns 
545661     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
547960     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.3s 
547960     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqSelfDefinitionEQ2 
548723     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqSelfDefinitionEQ2 
548734     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 8.73ms 
548735     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_indexOfSeqSingleton.proof 
548735     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 61.6ns 
548736     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
551031     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.3s 
551031     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: indexOfSeqSingleton 
551790     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: indexOfSeqSingleton 
551793     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.6ms 
551794     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_indexOfSeqConcatFirst.proof 
551794     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 44.7ns 
551795     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
554092     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.3s 
554092     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: indexOfSeqConcatFirst 
554852     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: indexOfSeqConcatFirst 
554869     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 14.76ms 
554870     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_indexOfSeqConcatSecond.proof 
554870     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 66.5ns 
554871     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
557188     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.32s 
557188     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: indexOfSeqConcatSecond 
557952     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: indexOfSeqConcatSecond 
557968     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 13.25ms 
557969     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_indexOfSeqSub.proof 
557969     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 62.3ns 
557969     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
560266     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.3s 
560267     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: indexOfSeqSub 
561025     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: indexOfSeqSub 
561043     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 15.5ms 
561044     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfArray2seq.proof 
561044     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 49.4ns 
561044     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
563341     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.3s 
563341     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfArray2seq 
564100     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfArray2seq 
564103     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.14ms 
564104     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getAnyOfArray2seq.proof 
564104     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 45.6ns 
564104     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
566395     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.29s 
566395     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getAnyOfArray2seq 
567157     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getAnyOfArray2seq 
567160     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.02ms 
567161     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfArray2seq.proof 
567161     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 54.7ns 
567162     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
569450     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.29s 
569450     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfArray2seq 
570209     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfArray2seq 
570215     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.59ms 
570216     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_getAnyOfNPermInv.proof 
570216     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 55ns 
570217     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
572527     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.31s 
572527     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getAnyOfNPermInv 
573285     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getAnyOfNPermInv 
573291     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4ms 
573292     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqNPermRange.proof 
573292     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 50.9ns 
573293     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
575587     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.29s 
575587     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqNPermRange 
576347     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqNPermRange 
576413     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 60.63ms 
576414     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermTrans.proof 
576414     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 60.4ns 
576415     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
578717     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.3s 
578717     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermTrans 
579478     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermTrans 
579503     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 21.95ms 
579504     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermRefl.proof 
579504     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 49.3ns 
579504     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
581817     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.31s 
581817     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermRefl 
582572     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermRefl 
582593     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 18.64ms 
582594     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermSplit.proof 
582594     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 57.6ns 
582595     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
584888     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.29s 
584888     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermSplit 
585647     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermSplit 
585648     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 272.6ns 
585650     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqNPermRight.proof 
585650     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 47.1ns 
585651     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
587963     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.31s 
587964     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqNPermRight 
588723     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqNPermRight 
588914     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 181.33ms 
588916     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermFromSwap.proof 
588916     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 110.4ns 
588917     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
591269     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.35s 
591270     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermFromSwap 
592032     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermFromSwap 
592079     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 42.92ms 
592081     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermTransAlt0.proof 
592081     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 62ns 
592081     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
594395     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.31s 
594395     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermTransAlt0 
595182     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermTransAlt0 
595185     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.68ms 
595186     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermTransAlt1.proof 
595187     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 46.1ns 
595187     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
597576     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.39s 
597576     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermTransAlt1 
598355     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermTransAlt1 
598357     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 310.9ns 
598358     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermTransAlt2.proof 
598358     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 55.1ns 
598359     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
600715     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.36s 
600715     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermTransAlt2 
601497     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermTransAlt2 
601499     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 317.5ns 
601500     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermTransAlt3.proof 
601501     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 45.2ns 
601501     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
603857     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.36s 
603857     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermTransAlt3 
604620     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermTransAlt3 
604622     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 452.9ns 
604623     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermForall.proof 
604623     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 50.1ns 
604624     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
606937     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.31s 
606937     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermForall 
607694     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermForall 
607787     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 91.31ms 
607789     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermExists.proof 
607789     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 209.6ns 
607790     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
610099     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.31s 
610099     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermExists 
610859     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermExists 
610920     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 58.54ms 
610921     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm2/Taclet_schiffl_lemma_2.proof 
610921     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 74.3ns 
610922     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
613245     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.32s 
613245     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: schiffl_lemma_2 
614004     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: schiffl_lemma_2 
614005     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.6ns 
614035     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 1: 'macro split-prop' 
614082     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 2: 'rule allRight' 
614105     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 3: 'rule allRight' 
614112     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 4: 'macro split-prop' 
614121     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 5: 'rule 'seqPermDefLeft'' 
614128     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 6: 'rule 'andLeft'' 
614129     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 7: 'rule 'exLeft'' 
614132     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 8: 'macro split-prop' 
614137     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 9: 'rule  seqNPermRange' 
614140     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 10: 'instantiate var=iv with='v_x_0' occ=1' 
614145     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 11: 'rule impLeft' 
614146     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 12: 'tryclose branch' 
614361     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 13: 'rule andLeft' 
614363     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 14: 'rule andLeft' 
614364     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 15: 'instantiate var=iv with='v_y_0' occ=1' 
614365     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 16: 'rule impLeft' 
614366     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 17: 'tryclose branch' 
614462     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 18: 'rule andLeft' 
614463     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 19: 'rule andLeft' 
614464     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 20: 'rule seqNPermDefLeft' 
614466     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 21: 'instantiate var=iv with='v_x_0' occ=2' 
614467     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 22: 'rule impLeft' 
614468     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 23: 'tryclose branch' 
614596     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 24: 'rule exLeft' 
614597     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 25: 'rule andLeft' 
614598     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 26: 'rule andLeft' 
614599     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 27: 'instantiate hide var=iv with='v_y_0' occ=2' 
614600     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 28: 'rule impLeft' 
614601     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 29: 'tryclose branch' 
614700     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 30: 'rule exLeft' 
614701     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 31: 'rule andLeft' 
614702     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 32: 'rule andLeft' 
614703     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 33: 'instantiate var=iv with='jv_0' occ=1' 
614704     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 34: 'rule impLeft' 
614705     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 35: 'tryclose branch' 
614710     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 36: 'rule andLeft' 
614711     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 37: 'rule andLeft' 
614712     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 38: 'rule castAdd formula='s_0[jv_0] = v_x_0' occ=0' 
614713     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 39: 'instantiate hide var=iv with='jv_1' occ=1' 
614714     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 40: 'rule impLeft' 
614715     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 41: 'tryclose branch' 
614720     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 42: 'rule andLeft' 
614721     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 43: 'rule andLeft' 
614722     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 44: 'rule castAdd formula='s_0[jv_1] = v_y_0' occ=0' 
614724     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 45: 'instantiate var=iv  with='v_x_0'' 
614724     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 46: 'rule impLeft' 
614725     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 47: 'tryclose branch' 
614841     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 48: 'instantiate var=iv  with='v_y_0'' 
614842     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 49: 'rule impLeft' 
614843     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 50: 'tryclose branch' 
614947     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 51: 'cut 'v_x_0 = v_y_0'' 
614949     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)'' 
614951     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 53: 'rule andRight' 
614952     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 54: 'rule andRight' 
614953     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 55: 'rule andRight' 
614953     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 56: 'rule andRight' 
614954     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 57: 'rule lenOfSwap' 
614955     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 58: 'tryclose branch' 
614960     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 59: 'rule seqNPermSwapNPerm' 
614961     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 60: 'instantiate hide var='iv' with='v_x_0' occ=1' 
614962     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 61: 'instantiate hide var='jv' with='jv_0'' 
614963     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 62: 'rule impLeft' 
614964     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 63: 'tryclose branch' 
615061     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 64: 'tryclose branch' 
615064     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 65: 'rule allRight' 
615065     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 66: 'rule impRight' 
615066     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 67: 'rule andLeft' 
615066     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 68: 'instantiate var=iv with='v_iv_0'' 
615067     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 69: 'rule impLeft' 
615068     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 70: 'tryclose branch' 
615171     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 71: 'rule getOfSwap' 
615172     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 72: 'rule ifthenelse_negated' 
615173     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 73: 'rule ifthenelse_split occ=0' 
615175     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 74: 'rule andLeft' 
615175     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 75: 'rule andLeft' 
615176     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 76: 'rule andLeft' 
615176     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 77: 'rule ifthenelse_split occ=0' 
615177     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 78: 'tryclose branch' 
615257     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 79: 'rule ifthenelse_split occ=0' 
615258     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 80: 'tryclose branch' 
615333     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 81: 'tryclose branch' 
615336     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 82: 'tryclose branch' 
615340     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 83: 'rule getOfSwap' 
615341     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 84: 'rule ifthenelse_negated' 
615342     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 85: 'rule ifthenelse_split occ=0' 
615343     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 86: 'rule andLeft' 
615344     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 87: 'rule andLeft' 
615344     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 88: 'rule andLeft' 
615345     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 89: 'rule ifthenelse_split occ=0' 
615346     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 90: 'tryclose branch' 
615353     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 91: 'tryclose branch' 
615356     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 92: 'tryclose branch' 
615439     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 93: 'rule getOfSwap' 
615441     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 94: 'rule ifthenelse_negated' 
615442     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 95: 'rule ifthenelse_split occ=0' 
615443     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 96: 'rule andLeft' 
615443     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 97: 'rule andLeft' 
615444     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 98: 'rule andLeft' 
615444     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 99: 'rule ifthenelse_split occ=0' 
615445     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 100: 'tryclose branch' 
615491     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 101: 'tryclose branch' 
615496     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 102: 'tryclose branch' 
615580     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 103: 'cut '(int)s_0[v_x_0] = (int)s_0[v_y_0]'' 
615581     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 104: 'rule seqNPermInjective' 
615583     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 105: 'instantiate hide var=iv with='v_x_0'' 
615584     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 106: 'instantiate hide var=jv with='v_y_0'' 
615585     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 107: 'rule impLeft' 
615586     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 108: 'tryclose branch' 
615739     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 109: 'tryclose branch' 
615742     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 110: 'cut '(int)s_0[v_x_0] = v_x_0'' 
615743     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)'' 
615745     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 112: 'rule andRight' 
615746     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 113: 'rule andRight' 
615746     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 114: 'rule andRight' 
615747     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 115: 'rule andRight' 
615748     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 116: 'tryclose branch' 
615755     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 117: 'rule seqNPermSwapNPerm' 
615756     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 118: 'instantiate hide var=iv with='v_y_0'' 
615758     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 119: 'instantiate hide var=jv with='jv_1'' 
615758     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 120: 'tryclose branch' 
615841     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 121: 'rule allRight' 
615842     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 122: 'rule impRight' 
615843     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 123: 'rule andLeft' 
615844     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 124: 'instantiate var=iv with='v_iv_0'' 
615844     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 125: 'rule impLeft' 
615845     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 126: 'tryclose branch' 
615935     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 127: 'rule getOfSwap' 
615936     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 128: 'rule ifthenelse_negated' 
615937     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 129: 'rule ifthenelse_split occ=0' 
615938     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 130: 'rule andLeft' 
615939     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 131: 'rule andLeft' 
615939     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 132: 'rule andLeft' 
615940     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 133: 'rule ifthenelse_split occ=0' 
615941     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 134: 'tryclose branch' 
616020     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 135: 'rule ifthenelse_split occ=0' 
616021     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 136: 'tryclose branch' 
616089     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 137: 'instantiate var=iv with='v_y_0'' 
616090     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 138: 'rule impLeft' 
616090     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 139: 'tryclose branch' 
616094     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 140: 'tryclose branch' 
616098     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 141: 'tryclose branch' 
616102     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 142: 'tryclose branch' 
616210     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 143: 'rule getOfSwap' 
616211     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 144: 'rule ifthenelse_negated' 
616212     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 145: 'rule ifthenelse_split occ=0' 
616213     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 146: 'tryclose branch' 
616221     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 147: 'tryclose branch' 
616298     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 148: 'tryclose branch' 
619813     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 149: 'cut  '(int)s_0[v_y_0] = v_y_0'' 
619814     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)'' 
619819     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 151: 'rule andRight' 
619820     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 152: 'rule andRight' 
619826     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 153: 'rule andRight' 
619826     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 154: 'rule andRight' 
619827     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 155: 'tryclose branch' 
619834     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 156: 'rule seqNPermSwapNPerm' 
619835     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 157: 'instantiate hide var=iv with='v_x_0'' 
619836     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 158: 'instantiate hide var=jv with='jv_0'' 
619837     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 159: 'rule impLeft' 
619838     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 160: 'tryclose branch' 
619925     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 161: 'tryclose branch' 
619928     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 162: 'rule allRight' 
619929     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 163: 'rule impRight' 
619930     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 164: 'rule andLeft' 
619930     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 165: 'instantiate var=iv with='v_iv_0'' 
619931     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 166: 'rule impLeft' 
619931     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 167: 'tryclose branch' 
620020     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 168: 'rule getOfSwap' 
620021     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 169: 'rule ifthenelse_negated' 
620021     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 170: 'rule ifthenelse_split occ=0' 
620022     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 171: 'rule andLeft' 
620023     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 172: 'rule andLeft' 
620023     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 173: 'rule andLeft' 
620023     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 174: 'rule ifthenelse_split occ=0' 
620024     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 175: 'tryclose branch' 
620096     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 176: 'rule ifthenelse_split occ=0' 
620097     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 177: 'tryclose branch' 
620166     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 178: 'tryclose branch' 
620170     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 179: 'tryclose branch' 
620174     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 180: 'rule getOfSwap' 
620175     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 181: 'rule ifthenelse_negated' 
620175     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 182: 'rule ifthenelse_split occ=0' 
620176     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 183: 'tryclose branch' 
620185     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 184: 'tryclose branch' 
620260     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 185: 'rule getOfSwap' 
620261     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 186: 'rule ifthenelse_negated' 
620261     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 187: 'rule ifthenelse_split occ=0' 
620262     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 188: 'tryclose branch' 
620331     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 189: 'tryclose branch' 
620339     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 190: 'cut '(int)s_0[v_x_0]=v_y_0'' 
620340     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)'' 
620341     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 192: 'rule andRight' 
620342     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 193: 'rule andRight' 
620342     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 194: 'rule andRight' 
620343     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 195: 'rule andRight' 
620343     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 196: 'tryclose branch' 
620353     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 197: 'rule seqNPermSwapNPerm' 
620354     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 198: 'instantiate hide var=iv with='jv_0'' 
620355     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 199: 'instantiate hide var=jv with='v_x_0'' 
620355     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 200: 'rule impLeft' 
620356     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 201: 'tryclose branch' 
620438     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 202: 'rule seqNPermSwapNPerm formula='seqNPerm(seqSwap(s_0, jv_0, v_x_0))'' 
620440     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 203: 'instantiate hide var=iv with='jv_0'' 
620440     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 204: 'instantiate hide var=jv with='v_y_0'' 
620441     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 205: 'rule impLeft' 
620442     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 206: 'tryclose branch' 
620532     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 207: 'tryclose branch' 
620536     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 208: 'rule allRight' 
620537     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 209: 'rule impRight' 
620537     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 210: 'rule andLeft' 
620538     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 211: 'instantiate var=iv with='v_iv_0'' 
620538     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 212: 'rule impLeft' 
620539     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 213: 'tryclose branch' 
620632     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 214: 'rule getOfSwap' 
620634     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 215: 'rule ifthenelse_negated' 
620634     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 216: 'rule ifthenelse_split occ=0' 
620635     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 217: 'rule andLeft' 
620636     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 218: 'rule andLeft' 
620636     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 219: 'rule andLeft' 
620636     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 220: 'rule ifthenelse_split occ=0' 
620637     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 221: 'rule getOfSwap' 
620638     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 222: 'rule ifthenelse_negated' 
620639     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 223: 'rule ifthenelse_split occ=0' 
620639     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 224: 'rule andLeft' 
620640     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 225: 'rule andLeft' 
620640     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 226: 'rule andLeft' 
620641     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 227: 'rule ifthenelse_split occ=0' 
620641     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 228: 'tryclose branch' 
620725     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 229: 'rule ifthenelse_split occ=0' 
620726     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 230: 'tryclose branch' 
620732     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 231: 'tryclose branch' 
620806     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 232: 'tryclose branch' 
620884     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 233: 'rule ifthenelse_split' 
620885     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 234: 'rule getOfSwap' 
620886     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 235: 'rule ifthenelse_negated' 
620886     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 236: 'rule ifthenelse_split occ=0' 
620887     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 237: 'rule andLeft' 
620888     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 238: 'rule andLeft' 
620888     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 239: 'rule andLeft' 
620888     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 240: 'rule ifthenelse_split occ=0' 
620889     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 241: 'tryclose branch' 
620971     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 242: 'tryclose branch' 
621013     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 243: 'tryclose branch' 
621098     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 244: 'rule getOfSwap' 
621099     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 245: 'rule ifthenelse_negated' 
621100     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 246: 'rule ifthenelse_split occ=0' 
621100     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 247: 'rule andLeft' 
621101     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 248: 'rule andLeft' 
621101     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 249: 'rule andLeft' 
621101     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 250: 'rule ifthenelse_split occ=0' 
621102     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 251: 'tryclose branch' 
621106     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 252: 'rule ifthenelse_split occ=0' 
621107     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 253: 'tryclose branch' 
621182     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 254: 'tryclose branch' 
621187     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 255: 'tryclose branch' 
621192     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 256: 'tryclose branch' 
621286     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 257: 'rule getOfSwap' 
621287     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 258: 'rule ifthenelse_negated' 
621287     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 259: 'rule ifthenelse_split occ=0' 
621288     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 260: 'rule andLeft' 
621289     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 261: 'rule andLeft' 
621289     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 262: 'rule andLeft' 
621289     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 263: 'rule ifthenelse_split occ=0' 
621290     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 264: 'tryclose branch' 
621341     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 265: 'rule ifthenelse_split occ=0' 
621342     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 266: 'rule getOfSwap' 
621343     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 267: 'rule ifthenelse_negated' 
621343     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 268: 'rule ifthenelse_split occ=0' 
621344     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 269: 'tryclose branch' 
621349     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 270: 'tryclose branch' 
621353     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 271: 'tryclose branch' 
621463     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 272: 'tryclose branch' 
621548     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 273: 'rule getOfSwap' 
621549     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 274: 'rule ifthenelse_negated' 
621550     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 275: 'rule ifthenelse_split occ=0' 
621550     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 276: 'tryclose branch' 
621711     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 277: 'tryclose branch' 
621795     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 278: 'cut 'int::seqGet(s_0, v_y_0)=v_x_0'' 
621795     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 279: 'tryclose branch' 
624713     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 280: 'rule seqNPermSwapNPerm' 
624718     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 281: 'instantiate hide var=iv with='jv_1'' 
624719     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 282: 'instantiate hide var=jv with='v_y_0'' 
624719     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 283: 'rule impLeft' 
624720     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 284: 'tryclose branch' 
624829     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 285: 'rule seqNPermSwapNPerm formula='seqNPerm(seqSwap(s_0,jv_1,v_y_0))'' 
624830     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 286: 'instantiate hide var=iv with='jv_1'' 
624831     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 287: 'instantiate hide var=jv with='v_x_0'' 
624832     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 288: 'rule impLeft' 
624832     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 289: 'tryclose branch' 
624932     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 290: 'tryclose branch' 
627828     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 291: 'tryclose branch' 
630875     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 292: 'rule seqNPermSwapNPerm formula='seqNPerm(s_0)'' 
630879     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 293: 'instantiate hide var=iv with='v_x_0'' 
630880     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 294: 'instantiate hide var=jv with='jv_0'' 
630881     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 295: 'rule impLeft' 
630882     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 296: 'tryclose branch' 
630989     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 297: 'rule seqNPermSwapNPerm formula='seqNPerm(seqSwap(s_0,v_x_0,jv_0))'' 
630990     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 298: 'instantiate hide var=iv with='v_y_0'' 
630991     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 299: 'instantiate hide var=jv with='jv_1'' 
630992     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)' ...' 
630994     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 301: 'tryclose branch' 
632094     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm2/Taclet_schiffl_thm_1.proof 
632094     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 76.5ns 
632095     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
634544     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.45s 
634544     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: schiffl_thm_1 
635322     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: schiffl_thm_1 
635323     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 6.1ns 
635324     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 1: 'macro split-prop' 
635329     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 2: 'rule schiffl_lemma_2 formula='seqPerm(f_s, f_t)'' 
635340     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 3: 'instantiate hide var=x with='f_x'' 
635342     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 4: 'instantiate hide var=y with='f_y'' 
635343     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 5: 'rule impLeft' 
635344     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 6: 'tryclose branch' 
635348     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 7: 'rule exLeft' 
635349     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 8: 'macro split-prop' 
635351     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 9: 'rule seqPermDef occ=1' 
635354     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 10: 'rule andRight' 
635354     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 11: 'tryclose branch' 
635362     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 12: 'instantiate hide var=s with='r_0'' 
635364     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 13: 'rule andRight' 
635364     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 14: 'tryclose branch' 
635451     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 15: 'rule allRight' 
635452     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 16: 'rule impRight' 
635453     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 17: 'instantiate hide var=iv with='iv_0'' 
635453     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 18: 'rule impLeft' 
635454     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 19: 'tryclose branch' 
635511     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 20: 'rule andLeft' 
635512     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 21: 'rule seqNPermRange' 
635513     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 22: 'instantiate hide var=iv with='iv_0'' 
635514     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 23: 'rule impLeft' 
635514     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 24: 'tryclose branch' 
635517     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 25: 'rule andLeft' 
635518     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 26: 'rule andLeft' 
635518     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 27: 'rule seqNPermRange' 
635519     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 28: 'instantiate hide var=iv with='f_x'' 
635520     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 29: 'rule impLeft' 
635521     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 30: 'tryclose branch' 
635596     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 31: 'rule andLeft' 
635596     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 32: 'rule andLeft' 
635597     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 33: 'rule seqNPermRange' 
635598     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 34: 'instantiate hide var=iv with='f_y'' 
635599     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 35: 'rule impLeft' 
635599     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 36: 'tryclose branch' 
635677     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 37: 'rule andLeft' 
635678     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 38: 'rule andLeft' 
635678     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 39: 'rule getOfSeqDef occ=0' 
635679     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 40: 'rule getOfSeqDef' 
635679     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 41: 'rule ifthenelse_split occ=0' 
635680     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 42: 'rule andLeft occ=0' 
635680     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 43: 'rule sub_zero_2 occ=0' 
635681     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 44: 'rule ifthenelse_split occ=2' 
635682     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 45: 'rule andLeft' 
635682     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 46: 'rule sub_zero_2 occ=0' 
635682     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 47: 'rule add_zero_right occ=0' 
635683     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 48: 'rule add_zero_right occ=0' 
635683     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 49: 'rule add_zero_right occ=0' 
635684     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 50: 'rule add_zero_right occ=0' 
635684     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 51: 'rule add_zero_right occ=0' 
635685     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 52: 'rule add_zero_right occ=0' 
635685     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 53: 'rule ifthenelse_split occ=0' 
635686     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 54: 'rule ifthenelse_split occ=0' 
635687     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 55: 'tryclose branch' 
635689     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 56: 'tryclose branch' 
635724     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 57: 'rule ifthenelse_split occ=0' 
635725     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 58: 'tryclose branch' 
635775     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 59: 'rule ifthenelse_split occ=0' 
635776     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 60: 'rule seqNPermInjective' 
635777     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 61: 'instantiate hide var=iv with='iv_0'' 
635778     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 62: 'instantiate hide var=jv with='f_y'' 
635779     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 63: 'rule impLeft' 
635779     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 64: 'tryclose branch' 
635825     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 65: 'tryclose branch' 
635827     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 66: 'rule ifthenelse_split occ=0' 
635828     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 67: 'rule seqNPermInjective' 
635829     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 68: 'instantiate hide var=iv with='iv_0'' 
635830     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 69: 'instantiate hide var=jv with='f_x'' 
635831     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 70: 'rule impLeft' 
635832     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 71: 'tryclose branch' 
635880     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 72: 'tryclose branch' 
635882     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 73: 'tryclose branch' 
635885     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 74: 'tryclose branch' 
635941     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 75: 'tryclose branch' 
635990     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_eqSameSeq.proof 
635990     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 200.2ns 
635991     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
638350     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.36s 
638351     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: eqSameSeq 
639149     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: eqSameSeq 
639179     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 26.77ms