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

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

tests
0

failures
0

ignored
10m31.65s

duration
100%

successful

Tests

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

Standard output

339        INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src/test/resources/testcase/dummyTrue.key 
365        DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 11.13ms 
572        INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
585        WARN  Test worker     d.u.i.k.s.ProofSettings   No proof-settings could be loaded, using defaults java.io.FileNotFoundException: /home/runner/.key/proof-settings.props (No such file or directory)
	at java.base/java.io.FileInputStream.open0(Native Method)

1534       DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for Meta 
1536       DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for Meta 
1540       DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for Meta 
1540       DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for Meta 
3276       DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for JavaBigintExpression 
8363       DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 7.79s 
8450       INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof dummyTrue.key 
8487       DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 37.2ns 
8501       INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/firstOrder/Taclet_eqTermCut.proof 
8502       DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 1.39ms 
8509       INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
11203      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.69s 
11206      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: eqTermCut 
12118      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: eqTermCut 
12142      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 18.22ms 
12152      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/firstOrder/Taclet_equivAllRight.proof 
12152      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 267.8ns 
12154      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
14758      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.6s 
14764      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: equivAllRight 
15669      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: equivAllRight 
15695      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 20.34ms 
15699      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_irrflConcrete1.proof 
15700      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 195.9ns 
15703      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
18272      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.57s 
18273      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: irrflConcrete1 
19126      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: irrflConcrete1 
19133      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.01ms 
19136      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_irrflConcrete2.proof 
19136      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 130.5ns 
19137      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
21536      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.4s 
21536      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: irrflConcrete2 
22386      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: irrflConcrete2 
22401      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 10.99ms 
22405      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_cancel_gtPos.proof 
22405      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 669.8ns 
22407      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
24779      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.37s 
24779      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: cancel_gtPos 
25560      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: cancel_gtPos 
25600      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 36.77ms 
25602      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_cancel_gtNeg.proof 
25602      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 172ns 
25603      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
27982      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.38s 
27982      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: cancel_gtNeg 
28735      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: cancel_gtNeg 
28774      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 34.65ms 
28782      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intRulesIgnoringOF/Taclet_moduloIntIsInInt.proof 
28782      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 595.1ns 
28784      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
31167      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.38s 
31168      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: moduloIntIsInInt 
31952      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: moduloIntIsInInt 
31956      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 721.8ns 
31963      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intRulesIgnoringOF/Taclet_moduloLongIsInLong.proof 
31964      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 360.4ns 
31966      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
34307      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.34s 
34308      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: moduloLongIsInLong 
35088      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: moduloLongIsInLong 
35091      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 632.6ns 
35093      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intRulesIgnoringOF/Taclet_moduloShortIsInShort.proof 
35094      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 358.1ns 
35095      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
37449      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.35s 
37449      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: moduloShortIsInShort 
38229      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: moduloShortIsInShort 
38232      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 576.2ns 
38234      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intRulesIgnoringOF/Taclet_moduloByteIsInByte.proof 
38235      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 276.7ns 
38236      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
40571      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.34s 
40572      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: moduloByteIsInByte 
41341      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: moduloByteIsInByte 
41344      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 585.6ns 
41345      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intRulesIgnoringOF/Taclet_moduloCharIsInChar.proof 
41346      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 127.6ns 
41347      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
43672      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.33s 
43672      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: moduloCharIsInChar 
44438      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: moduloCharIsInChar 
44441      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 537.3ns 
44443      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_div_unique1.proof 
44443      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 277.2ns 
44444      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
46782      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.34s 
46783      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: div_unique1 
47527      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: div_unique1 
47567      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 35.22ms 
47569      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_div_unique2.proof 
47569      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 137ns 
47573      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
49936      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.36s 
49936      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: div_unique2 
50700      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: div_unique2 
50733      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 30.11ms 
50735      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_div_exists.proof 
50735      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 140.2ns 
50736      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
53055      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.32s 
53056      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: div_exists 
53819      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: div_exists 
54002      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 173.37ms 
54006      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_div_one.proof 
54007      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 513.6ns 
54008      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
56327      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.32s 
56328      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: div_one 
57090      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: div_one 
57095      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3ms 
57097      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdiv_one.proof 
57097      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 135.5ns 
57098      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
59410      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.31s 
59411      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdiv_one 
60177      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdiv_one 
60181      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.35ms 
60185      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_div_zero.proof 
60185      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 334.7ns 
60187      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
62502      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.32s 
62504      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: div_zero 
63240      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: div_zero 
63279      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 33.6ms 
63281      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divResZero1.proof 
63281      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 204.1ns 
63282      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
65631      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.35s 
65631      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divResZero1 
66366      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divResZero1 
66382      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 12.93ms 
66384      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divResZero2.proof 
66384      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 207.4ns 
66385      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
68730      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.34s 
68731      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divResZero2 
69497      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divResZero2 
69513      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 13.33ms 
69515      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divResOne1.proof 
69515      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 130.2ns 
69520      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
71833      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.31s 
71833      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divResOne1 
72602      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divResOne1 
72623      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 17.46ms 
72625      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divResOne2.proof 
72625      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 146.9ns 
72628      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
74959      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.33s 
74959      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divResOne2 
75721      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divResOne2 
75739      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 14.49ms 
75745      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_div_cancel1.proof 
75748      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 2.41ms 
75749      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
78053      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.3s 
78053      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: div_cancel1 
78811      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: div_cancel1 
78836      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 20.86ms 
78838      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_div_cancel2.proof 
78838      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 132.3ns 
78839      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
81172      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.33s 
81173      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: div_cancel2 
81904      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: div_cancel2 
81907      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.3ms 
81908      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divAddMultDenom.proof 
81908      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 85.4ns 
81909      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
84237      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.33s 
84238      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divAddMultDenom 
84998      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divAddMultDenom 
85038      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 33.88ms 
85040      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divMinus.proof 
85041      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 353.2ns 
85042      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
87363      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.32s 
87363      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divMinus 
88133      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divMinus 
88187      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 47.74ms 
88189      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divMinusDenom.proof 
88189      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 122ns 
88190      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
90483      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.29s 
90484      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divMinusDenom 
91243      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divMinusDenom 
91285      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 36.39ms 
91287      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divLeastDPos.proof 
91287      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 131ns 
91288      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
93579      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.29s 
93581      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divLeastDPos 
94339      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divLeastDPos 
94346      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 5.14ms 
94350      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divLeastDNeg.proof 
94350      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 310ns 
94351      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
96679      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.33s 
96680      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divLeastDNeg 
97411      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divLeastDNeg 
97423      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 9.78ms 
97424      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divGreatestDPos.proof 
97425      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 102.1ns 
97425      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
99734      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.31s 
99734      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divGreatestDPos 
100463     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divGreatestDPos 
100473     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 8.18ms 
100475     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divGreatestDNeg.proof 
100475     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 93.6ns 
100476     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
102782     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.31s 
102782     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divGreatestDNeg 
103535     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divGreatestDNeg 
103543     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 5.53ms 
103544     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divIncreasingPos.proof 
103544     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 93.7ns 
103545     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
105832     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.29s 
105832     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divIncreasingPos 
106587     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divIncreasingPos 
106594     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 5.65ms 
106596     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divIncreasingNeg.proof 
106596     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 92.7ns 
106597     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
108908     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.31s 
108909     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divIncreasingNeg 
109664     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divIncreasingNeg 
109674     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 8.03ms 
109675     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdiv_zero.proof 
109676     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 118.5ns 
109676     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
111993     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.32s 
111993     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdiv_zero 
112783     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdiv_zero 
112787     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.5ms 
112788     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdivPulloutMinusNum.proof 
112788     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 166.5ns 
112789     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
115109     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.32s 
115110     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdivPulloutMinusNum 
115838     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdivPulloutMinusNum 
115849     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 8.91ms 
115851     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdivPulloutMinusDenom.proof 
115851     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 187.6ns 
115852     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
118164     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.31s 
118164     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdivPulloutMinusDenom 
118924     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdivPulloutMinusDenom 
118977     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 47.84ms 
118980     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdiv_uniquePosPos.proof 
118980     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 338.8ns 
118982     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
121278     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.3s 
121279     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdiv_uniquePosPos 
122036     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdiv_uniquePosPos 
122054     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 14.42ms 
122055     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdiv_uniquePosNeg.proof 
122056     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 106.4ns 
122056     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
124362     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.31s 
124362     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdiv_uniquePosNeg 
125117     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdiv_uniquePosNeg 
125135     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 15.1ms 
125137     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdiv_uniqueNegPos.proof 
125137     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 105.4ns 
125138     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
127435     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.3s 
127435     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdiv_uniqueNegPos 
128199     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdiv_uniqueNegPos 
128217     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 14.74ms 
128218     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdiv_uniqueNegNeg.proof 
128218     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 128.2ns 
128219     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
130532     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.31s 
130532     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdiv_uniqueNegNeg 
131261     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdiv_uniqueNegNeg 
131279     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 14.42ms 
131280     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdivMultDenom1.proof 
131280     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 116.8ns 
131281     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
133585     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.3s 
133585     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdivMultDenom1 
134314     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdivMultDenom1 
134355     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 36.54ms 
134357     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdivMultDenom2.proof 
134359     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 1.88ms 
134361     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
136683     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.32s 
136683     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdivMultDenom2 
137440     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdivMultDenom2 
137445     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.37ms 
137446     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_mod_geZero.proof 
137446     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 79.5ns 
137447     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
139753     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.31s 
139753     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: mod_geZero 
140510     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: mod_geZero 
140514     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.59ms 
140515     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_mod_lessDenom.proof 
140515     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 96.7ns 
140516     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
142800     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.28s 
142801     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: mod_lessDenom 
143558     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: mod_lessDenom 
143567     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 6.12ms 
143568     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmod_NumPos.proof 
143568     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 88.7ns 
143569     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
145860     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.29s 
145860     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmod_NumPos 
146617     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmod_NumPos 
146625     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 6.03ms 
146627     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmod_NumNeg.proof 
146627     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 166.1ns 
146628     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
148935     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.31s 
148935     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmod_NumNeg 
149664     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmod_NumNeg 
149701     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 33.57ms 
149703     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmod_geZero.proof 
149703     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 177.5ns 
149704     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
152006     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.3s 
152007     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmod_geZero 
152765     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmod_geZero 
152774     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 7.11ms 
152775     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmodNumZero.proof 
152775     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 73.8ns 
152776     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
155063     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.29s 
155063     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmodNumZero 
155822     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmodNumZero 
155825     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.29ms 
155826     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmod_pulloutminusNum.proof 
155826     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 115ns 
155827     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
158213     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.39s 
158213     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmod_pulloutminusNum 
158974     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmod_pulloutminusNum 
158978     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.91ms 
158980     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmod_pulloutminusDenom.proof 
158980     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 83.9ns 
158980     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
161262     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.28s 
161262     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmod_pulloutminusDenom 
162013     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmod_pulloutminusDenom 
162017     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.46ms 
162019     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmodUnique1.proof 
162019     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 81.6ns 
162020     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
164299     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.28s 
164300     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmodUnique1 
165058     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmodUnique1 
165135     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 66.52ms 
165137     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmodUnique2.proof 
165138     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 308.1ns 
165139     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
167460     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.32s 
167461     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmodUnique2 
168191     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmodUnique2 
168271     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 71.84ms 
168273     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_intDivRem.proof 
168274     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 294.9ns 
168275     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
170583     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.31s 
170583     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: intDivRem 
171337     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: intDivRem 
171341     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.11ms 
171342     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmodjmod.proof 
171342     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 180.5ns 
171343     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
173631     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.29s 
173632     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmodjmod 
174382     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmodjmod 
174418     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 31.84ms 
174419     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmodDivisible.proof 
174420     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 308.1ns 
174421     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
176705     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.28s 
176705     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmodDivisible 
177460     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmodDivisible 
177499     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 35.04ms 
177500     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmodDivisibleRep.proof 
177500     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 108.4ns 
177501     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
179791     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.29s 
179791     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmodDivisibleRep 
180543     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmodDivisibleRep 
180547     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.28ms 
180554     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdivAddMultDenom.proof 
180554     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 85ns 
180555     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
182868     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.31s 
182868     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 
183758     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 148.25ms 
183761     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmodAltZero.proof 
183762     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 296.1ns 
183763     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
186092     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.33s 
186092     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmodAltZero 
186867     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmodAltZero 
186880     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 10.42ms 
186883     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmodAddMultDenomZero.proof 
186883     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 251.7ns 
186886     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
189183     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.3s 
189183     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmodAddMultDenomZero 
189934     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmodAddMultDenomZero 
189942     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 6.25ms 
189944     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_polyDiv_zero.proof 
189944     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 75.9ns 
189944     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
192223     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.28s 
192223     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: polyDiv_zero 
192976     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: polyDiv_zero 
192995     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 16.33ms 
192998     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_polyMod_ltdivDenom.proof 
193001     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 2.96ms 
193003     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
195286     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.28s 
195289     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: polyMod_ltdivDenom 
196044     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: polyMod_ltdivDenom 
196057     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 6.3ms 
196060     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_empty.proof 
196060     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 257.4ns 
196061     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
198355     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.29s 
198356     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_empty 
199082     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_empty 
199086     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.68ms 
199088     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_induction_upper.proof 
199088     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 143.9ns 
199089     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
201385     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.3s 
201385     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_upper 
202118     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_induction_upper 
202126     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 6.52ms 
202130     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_induction_lower.proof 
202130     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 273.7ns 
202131     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
204432     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.3s 
204432     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_lower 
205184     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_induction_lower 
205208     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 20.49ms 
205209     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_bounds.proof 
205209     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 75.6ns 
205210     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
207502     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.29s 
207503     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_bounds 
208254     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_bounds 
208270     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 13.49ms 
208271     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_bounds2.proof 
208271     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 74.9ns 
208272     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
210557     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.28s 
210557     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_bounds2 
211311     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_bounds2 
211327     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 13.07ms 
211328     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_induction_upper2.proof 
211329     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 86.5ns 
211329     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
213607     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.28s 
213607     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 
214365     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.8ms 
214367     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_induction_upper_concrete.proof 
214367     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 232.9ns 
214368     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
216670     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.3s 
216670     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_upper_concrete 
217398     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_induction_upper_concrete 
217402     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.67ms 
217404     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_induction_upper_concrete_2.proof 
217404     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 81.9ns 
217404     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
219705     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.3s 
219705     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_upper_concrete_2 
220461     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_induction_upper_concrete_2 
220467     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.52ms 
220468     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_induction_upper2_concrete.proof 
220468     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 88.5ns 
220469     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
222753     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.28s 
222753     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_upper2_concrete 
223503     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_induction_upper2_concrete 
223507     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.44ms 
223508     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_induction_lower_concrete.proof 
223508     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 67.2ns 
223509     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
225799     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.29s 
225799     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_lower_concrete 
226551     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_induction_lower_concrete 
226553     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 700.21ns 
226555     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_induction_lower2.proof 
226555     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 93.7ns 
226556     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
228841     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.28s 
228841     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_lower2 
229598     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_induction_lower2 
229602     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.26ms 
229603     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_induction_lower2_concrete.proof 
229604     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 86.7ns 
229604     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
231897     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.29s 
231898     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_lower2_concrete 
232649     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_induction_lower2_concrete 
232652     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.03ms 
232653     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_positive.proof 
232653     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 56ns 
232654     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
234964     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.31s 
234964     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_positive 
235693     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_positive 
235740     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 44.23ms 
235741     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_upper_bound.proof 
235742     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 95.7ns 
235742     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
238055     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.31s 
238056     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_upper_bound 
238809     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_upper_bound 
238845     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 33.39ms 
238848     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_lower_bound.proof 
238848     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 248.2ns 
238849     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
241157     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.31s 
241157     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_lower_bound 
241910     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_lower_bound 
241946     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 31.64ms 
241950     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_positive_lower_bound_element.proof 
241950     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 297.2ns 
241951     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
244236     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.28s 
244236     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_positive_lower_bound_element 
244987     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_positive_lower_bound_element 
245033     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 41.25ms 
245034     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_sub_same_index.proof 
245035     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 92.5ns 
245035     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
247332     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.3s 
247332     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_sub_same_index 
248091     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_sub_same_index 
248123     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 29.31ms 
248125     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_less_same_index.proof 
248125     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 94.2ns 
248126     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
250436     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.31s 
250436     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_less_same_index 
251163     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_less_same_index 
251213     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 44.62ms 
251214     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_equal_except_one_index.proof 
251214     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 73.3ns 
251215     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
253542     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.33s 
253542     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_equal_except_one_index 
254293     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_equal_except_one_index 
254319     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 23.62ms 
254321     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_is_max.proof 
254321     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 77.3ns 
254322     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
256599     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.28s 
256599     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_is_max 
257352     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_is_max 
257377     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 22.16ms 
257378     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_is_max2.proof 
257378     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 86.8ns 
257379     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
259664     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.28s 
259664     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_is_max2 
260417     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_is_max2 
260441     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 20.68ms 
260444     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_is_max3.proof 
260444     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 231.3ns 
260445     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
262731     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.29s 
262732     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_is_max3 
263484     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_is_max3 
263503     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 16.54ms 
263506     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_is_max4.proof 
263506     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 245.7ns 
263507     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
265804     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.3s 
265804     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_is_max4 
266532     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_is_max4 
266559     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 23.64ms 
266560     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_lt_max.proof 
266560     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 86.6ns 
266561     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
268861     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.3s 
268862     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_lt_max 
269590     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_lt_max 
269615     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 21.42ms 
269616     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_lt_max2.proof 
269616     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 101.9ns 
269617     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
271914     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.3s 
271914     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_lt_max2 
272668     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_lt_max2 
272698     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 25.64ms 
272700     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_lt_max3.proof 
272700     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 214.7ns 
272703     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
274983     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.28s 
274983     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_lt_max3 
275739     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_lt_max3 
275763     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 21.3ms 
275764     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_lt_max4.proof 
275764     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 85ns 
275765     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
278040     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.28s 
278040     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_lt_max4 
278795     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_lt_max4 
278815     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 17.59ms 
278817     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_gt0.proof 
278817     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 79.9ns 
278818     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
281091     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.27s 
281091     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_gt0 
281842     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_gt0 
281868     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 22.83ms 
281869     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_gt0_alt.proof 
281869     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 87.4ns 
281870     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
284175     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.31s 
284176     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_gt0_alt 
284904     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_gt0_alt 
284931     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 24.29ms 
284933     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_add_concrete.proof 
284933     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 100ns 
284934     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
287254     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.32s 
287254     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_add_concrete 
288007     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_add_concrete 
288015     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 5.94ms 
288016     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bprod/Taclet_bprod_all_positive.proof 
288016     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 68.3ns 
288017     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
290299     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.28s 
290299     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bprod_all_positive 
291053     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bprod_all_positive 
291071     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 15.11ms 
291072     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bprod/Taclet_bprod_split.proof 
291072     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 66.1ns 
291073     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
293348     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.28s 
293348     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bprod_split 
294101     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bprod_split 
294106     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.13ms 
294107     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powConcrete0.proof 
294107     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 83.8ns 
294108     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
296379     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.27s 
296379     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powConcrete0 
297130     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powConcrete0 
297132     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 673.21ns 
297134     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powConcrete1.proof 
297134     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 56ns 
297135     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
299433     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.3s 
299433     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powConcrete1 
300161     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powConcrete1 
300163     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 770.11ns 
300165     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powSplitFactor.proof 
300165     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 79.3ns 
300165     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
302456     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.29s 
302456     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powSplitFactor 
303185     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powSplitFactor 
303192     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.91ms 
303193     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powAdd.proof 
303193     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 58.7ns 
303194     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
305500     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.31s 
305500     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powAdd 
306251     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powAdd 
306258     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.77ms 
306259     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powMono.proof 
306260     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 88ns 
306260     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
308538     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.28s 
308538     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powMono 
309289     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powMono 
309302     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 10.23ms 
309303     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powMonoConcrete.proof 
309303     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 87.9ns 
309304     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
311574     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.27s 
311574     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powMonoConcrete 
312325     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powMonoConcrete 
312328     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.02ms 
312330     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powMonoConcreteRight.proof 
312330     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 75.9ns 
312331     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
314600     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.27s 
314600     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powMonoConcreteRight 
315351     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powMonoConcreteRight 
315353     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 572.1ns 
315355     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powPositive.proof 
315355     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 77.4ns 
315355     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
317649     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.29s 
317649     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powPositive 
318377     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powPositive 
318385     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.37ms 
318386     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powPositiveConcrete.proof 
318387     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 168.1ns 
318388     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
320687     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.3s 
320688     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powPositiveConcrete 
321440     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powPositiveConcrete 
321442     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 696.2ns 
321444     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powGeq1Concrete.proof 
321444     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 69.1ns 
321444     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
323716     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.27s 
323716     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powGeq1Concrete 
324476     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powGeq1Concrete 
324478     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 898.61ns 
324482     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_pow2InIntLower.proof 
324483     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 226.2ns 
324485     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
326767     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.28s 
326767     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: pow2InIntLower 
327520     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: pow2InIntLower 
327523     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 626.2ns 
327525     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_pow2InIntUpper.proof 
327525     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 206.9ns 
327526     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
329797     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.27s 
329798     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: pow2InIntUpper 
330550     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: pow2InIntUpper 
330555     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.21ms 
330557     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logSelfConcrete.proof 
330557     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 237.9ns 
330558     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
332829     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.27s 
332829     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logSelfConcrete 
333581     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logSelfConcrete 
333591     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 7.51ms 
333592     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_log1Concrete.proof 
333592     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 72.5ns 
333593     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
335886     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.29s 
335886     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: log1Concrete 
336613     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: log1Concrete 
336617     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.57ms 
336619     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logProduct.proof 
336619     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 83.6ns 
336620     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
338914     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.29s 
338914     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logProduct 
339671     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logProduct 
339678     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 5.46ms 
339680     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logTimesBaseConcrete.proof 
339680     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 73.2ns 
339680     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
341982     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.3s 
341982     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logTimesBaseConcrete 
342739     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logTimesBaseConcrete 
342749     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 7.34ms 
342753     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logProdIdentity.proof 
342754     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 243.1ns 
342756     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
345056     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.3s 
345056     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logProdIdentity 
345808     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logProdIdentity 
345824     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 13.32ms 
345825     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logProdIdentityConcrete.proof 
345825     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 71.7ns 
345826     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
348110     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.28s 
348110     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logProdIdentityConcrete 
348863     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logProdIdentityConcrete 
348867     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.86ms 
348868     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logPowIdentity.proof 
348868     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 65.6ns 
348869     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
351175     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.31s 
351175     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logPowIdentity 
351908     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logPowIdentity 
351912     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.27ms 
351913     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logPowIdentityConcrete.proof 
351913     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 65ns 
351914     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
354216     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.3s 
354217     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logPowIdentityConcrete 
354946     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logPowIdentityConcrete 
354950     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.24ms 
354951     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logPositive.proof 
354951     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 66.9ns 
354952     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
357259     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.31s 
357259     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logPositive 
358018     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logPositive 
358036     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 14.84ms 
358038     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logPositiveConcrete.proof 
358038     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 225.3ns 
358039     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
360336     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.3s 
360336     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logPositiveConcrete 
361089     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logPositiveConcrete 
361094     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 591.3ns 
361096     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logMono.proof 
361096     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 80.7ns 
361097     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
363374     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.28s 
363375     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logMono 
364124     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logMono 
364163     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 34.6ms 
364164     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logMonoConcrete.proof 
364165     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 82.4ns 
364165     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
366447     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.28s 
366448     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logMonoConcrete 
367203     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logMonoConcrete 
367207     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.91ms 
367208     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powLogLess.proof 
367208     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 67.2ns 
367209     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
369509     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.3s 
369509     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powLogLess 
370243     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powLogLess 
370266     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 19.1ms 
370268     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powLogMore2.proof 
370268     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 226.2ns 
370269     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
372598     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.33s 
372598     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powLogMore2 
373352     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powLogMore2 
373373     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 18.3ms 
373374     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logLessThanPow.proof 
373374     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 71.6ns 
373375     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
375653     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.28s 
375653     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logLessThanPow 
376405     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logLessThanPow 
376430     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 21.36ms 
376431     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logLessThanPowConcrete.proof 
376432     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 97.1ns 
376432     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
378713     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.28s 
378713     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logLessThanPowConcrete 
379471     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logLessThanPowConcrete 
379473     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 598.8ns 
379476     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logSqueeze.proof 
379476     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 242.3ns 
379477     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
381776     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.3s 
381776     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logSqueeze 
382504     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logSqueeze 
382510     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.95ms 
382511     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/booleanRules/Taclet_ifthenelse_equals.proof 
382511     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 73ns 
382512     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
384815     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.3s 
384815     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: ifthenelse_equals 
385571     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: ifthenelse_equals 
385575     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.52ms 
385576     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/booleanRules/Taclet_ifthenelse_equals_1.proof 
385576     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 73.5ns 
385577     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
387868     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.29s 
387868     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: ifthenelse_equals_1 
388622     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: ifthenelse_equals_1 
388625     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 880.41ns 
388626     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/booleanRules/Taclet_ifthenelse_equals_2.proof 
388626     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 54.7ns 
388627     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
390907     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.28s 
390907     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: ifthenelse_equals_2 
391664     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: ifthenelse_equals_2 
391667     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 888.21ns 
391668     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/locSet/Taclet_disjointWithSingleton1.proof 
391668     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 72.1ns 
391669     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
393965     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.3s 
393966     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: disjointWithSingleton1 
394700     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: disjointWithSingleton1 
394703     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.62ms 
394705     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/locSet/Taclet_disjointWithSingleton2.proof 
394705     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 65.6ns 
394705     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
397011     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.31s 
397011     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: disjointWithSingleton2 
397770     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: disjointWithSingleton2 
397774     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.95ms 
397779     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/locSet/Taclet_disjointArrayRanges.proof 
397779     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 237.1ns 
397780     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
400058     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.28s 
400058     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: disjointArrayRanges 
400816     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: disjointArrayRanges 
400827     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 7.8ms 
400828     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/locSet/Taclet_disjointArrayRangeAllFields1.proof 
400828     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 84.8ns 
400829     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
403108     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.28s 
403108     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: disjointArrayRangeAllFields1 
403867     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: disjointArrayRangeAllFields1 
403884     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 14.31ms 
403892     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/locSet/Taclet_disjointArrayRangeAllFields2.proof 
403892     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 246ns 
403893     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
406196     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.3s 
406196     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: disjointArrayRangeAllFields2 
406961     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: disjointArrayRangeAllFields2 
406973     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 9.45ms 
406974     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqSelfDefinition.proof 
406974     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 73.1ns 
406975     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
409260     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.28s 
409260     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqSelfDefinition 
410023     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqSelfDefinition 
410037     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 11.22ms 
410039     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqOutsideValue.proof 
410039     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 222.5ns 
410040     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
412317     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.28s 
412317     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqOutsideValue 
413080     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqOutsideValue 
413084     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.78ms 
413085     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_castedGetAny.proof 
413085     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 67.4ns 
413086     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
415383     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.3s 
415383     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: castedGetAny 
416148     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: castedGetAny 
416154     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.58ms 
416155     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqGetAlphaCast.proof 
416156     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 79.1ns 
416156     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
418439     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.28s 
418439     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqGetAlphaCast 
419203     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqGetAlphaCast 
419206     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 824.31ns 
419207     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqSingleton.proof 
419207     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 57ns 
419208     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
421482     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.27s 
421482     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqSingleton 
422246     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqSingleton 
422249     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.52ms 
422250     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqSingletonConcrete.proof 
422250     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 65.2ns 
422251     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
424545     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.29s 
424545     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqSingletonConcrete 
425310     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqSingletonConcrete 
425313     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 950.11ns 
425314     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqConcat.proof 
425314     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 76.3ns 
425315     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
427591     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.28s 
427592     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqConcat 
428357     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqConcat 
428369     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 10ms 
428371     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqSub.proof 
428371     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 59.8ns 
428372     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
430679     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.31s 
430679     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqSub 
431420     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqSub 
431425     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.55ms 
431426     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqReverse.proof 
431426     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 81.4ns 
431427     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
433720     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.29s 
433721     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqReverse 
434483     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqReverse 
434491     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 5ms 
434493     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqEmpty.proof 
434493     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 194.3ns 
434494     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
436775     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.28s 
436775     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqEmpty 
437542     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqEmpty 
437544     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 755.8ns 
437545     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqSingleton.proof 
437545     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 77.2ns 
437546     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
439847     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.3s 
439847     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqSingleton 
440610     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqSingleton 
440613     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 663.61ns 
440614     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqConcat.proof 
440614     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 68.2ns 
440615     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
442904     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.29s 
442904     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqConcat 
443669     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqConcat 
443673     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.28ms 
443674     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqSub.proof 
443674     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 79.1ns 
443675     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
445974     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.3s 
445974     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqSub 
446741     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqSub 
446744     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.35ms 
446746     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqReverse.proof 
446746     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 66.3ns 
446746     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
449020     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.27s 
449020     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqReverse 
449784     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqReverse 
449787     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.49ms 
449788     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_equalityToSeqGetAndSeqLenLeft.proof 
449789     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 64.7ns 
449789     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
452083     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.29s 
452083     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: equalityToSeqGetAndSeqLenLeft 
452823     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: equalityToSeqGetAndSeqLenLeft 
452826     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.32ms 
452828     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_equalityToSeqGetAndSeqLenRight.proof 
452828     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 63.1ns 
452828     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
455127     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.3s 
455128     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: equalityToSeqGetAndSeqLenRight 
455891     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: equalityToSeqGetAndSeqLenRight 
455897     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.79ms 
455898     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqSingletonEQ.proof 
455898     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 70ns 
455899     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
458203     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.3s 
458204     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqSingletonEQ 
458945     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqSingletonEQ 
458949     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.72ms 
458950     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqConcatEQ.proof 
458950     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 82.9ns 
458951     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
461253     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.3s 
461253     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqConcatEQ 
462017     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqConcatEQ 
462028     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 9.14ms 
462030     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqSubEQ.proof 
462030     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 77.9ns 
462031     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
464331     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.3s 
464331     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqSubEQ 
465073     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqSubEQ 
465075     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 772.21ns 
465076     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqReverseEQ.proof 
465076     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 67.1ns 
465077     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
467382     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.3s 
467382     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqReverseEQ 
468151     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqReverseEQ 
468159     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 5.41ms 
468160     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqEmptyEQ.proof 
468160     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 66.3ns 
468161     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
470465     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.3s 
470465     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqEmptyEQ 
471205     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqEmptyEQ 
471208     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.13ms 
471209     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqSingletonEQ.proof 
471209     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 53.4ns 
471210     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
473507     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.3s 
473507     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqSingletonEQ 
474272     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqSingletonEQ 
474275     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 865.81ns 
474276     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqConcatEQ.proof 
474276     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 89.2ns 
474277     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
476570     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.29s 
476570     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqConcatEQ 
477312     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqConcatEQ 
477317     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.2ms 
477318     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqSubEQ.proof 
477318     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 79.8ns 
477319     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
479634     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.31s 
479634     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqSubEQ 
480400     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqSubEQ 
480403     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.55ms 
480404     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqReverseEQ.proof 
480405     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 78.5ns 
480405     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
482709     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.3s 
482709     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqReverseEQ 
483473     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqReverseEQ 
483476     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.82ms 
483478     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqDefEQ.proof 
483478     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 66.5ns 
483478     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
485760     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.28s 
485760     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqDefEQ 
486523     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqDefEQ 
486527     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.18ms 
486529     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqDefEQ.proof 
486529     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 71.7ns 
486529     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
488834     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.3s 
488834     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqDefEQ 
489598     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqDefEQ 
489604     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.62ms 
489605     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqConcatWithSeqEmpty1.proof 
489605     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 84.4ns 
489606     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
491913     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.31s 
491913     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqConcatWithSeqEmpty1 
492655     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqConcatWithSeqEmpty1 
492669     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 12.3ms 
492670     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqConcatWithSeqEmpty2.proof 
492671     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 85.4ns 
492671     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
494971     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.3s 
494971     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqConcatWithSeqEmpty2 
495738     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqConcatWithSeqEmpty2 
495754     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 13.63ms 
495755     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqReverseOfSeqEmpty.proof 
495756     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 76.7ns 
495756     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
498055     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.3s 
498055     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqReverseOfSeqEmpty 
498820     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqReverseOfSeqEmpty 
498830     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 8.78ms 
498832     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_subSeqComplete.proof 
498832     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 74.7ns 
498833     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
501115     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.28s 
501115     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: subSeqComplete 
501881     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: subSeqComplete 
501891     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 8.9ms 
501893     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_subSeqTailR.proof 
501893     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 81.5ns 
501894     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
504201     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.31s 
504201     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: subSeqTailR 
504970     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: subSeqTailR 
504996     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 23.51ms 
504997     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_subSeqTailL.proof 
504997     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 80.1ns 
504998     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
507308     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.31s 
507309     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: subSeqTailL 
508073     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: subSeqTailL 
508098     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 23.11ms 
508099     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_subSeqTailEQR.proof 
508099     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 83.5ns 
508100     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
510398     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.3s 
510398     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: subSeqTailEQR 
511143     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: subSeqTailEQR 
511168     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 22.12ms 
511169     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_subSeqTailEQL.proof 
511169     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 76.1ns 
511170     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
513472     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.3s 
513472     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: subSeqTailEQL 
514237     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: subSeqTailEQL 
514251     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 12.52ms 
514253     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDef_split.proof 
514253     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 61.3ns 
514253     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
516551     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.3s 
516551     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_split 
517317     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDef_split 
517352     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 32.03ms 
517355     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDef_induction_upper.proof 
517355     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 215.2ns 
517356     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
519653     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.3s 
519653     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_induction_upper 
520420     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDef_induction_upper 
520468     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 43.7ms 
520469     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDef_induction_upper_concrete.proof 
520469     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 85.7ns 
520470     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
522751     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.28s 
522751     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_induction_upper_concrete 
523517     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDef_induction_upper_concrete 
523556     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 35.78ms 
523557     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDef_induction_lower.proof 
523557     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 87.2ns 
523558     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
525857     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.3s 
525857     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_induction_lower 
526624     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDef_induction_lower 
526666     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 38.77ms 
526667     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDef_induction_lower_concrete.proof 
526668     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 87.5ns 
526668     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
528973     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.3s 
528973     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_induction_lower_concrete 
529739     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDef_induction_lower_concrete 
529784     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 41.48ms 
529786     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDef_split_in_three.proof 
529786     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 79.5ns 
529787     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
532091     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.3s 
532091     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_split_in_three 
532859     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDef_split_in_three 
532980     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 113.57ms 
532982     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDef_empty.proof 
532982     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 90.3ns 
532983     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
535294     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.31s 
535294     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_empty 
536068     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDef_empty 
536078     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 7.24ms 
536082     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDef_one_summand.proof 
536082     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 88.6ns 
536083     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
538370     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.29s 
538370     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_one_summand 
539138     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDef_one_summand 
539146     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 5.8ms 
539147     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDef_lower_equals_upper.proof 
539147     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 121.6ns 
539148     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
541450     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.3s 
541450     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_lower_equals_upper 
542218     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDef_lower_equals_upper 
542223     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.62ms 
542224     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDefOfSeq.proof 
542224     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 75.1ns 
542225     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
544524     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.3s 
544524     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDefOfSeq 
545291     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDefOfSeq 
545310     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 15.34ms 
545311     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqSelfDefinitionEQ2.proof 
545312     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 91.5ns 
545312     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
547615     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.3s 
547615     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqSelfDefinitionEQ2 
548381     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqSelfDefinitionEQ2 
548392     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 8.92ms 
548393     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_indexOfSeqSingleton.proof 
548394     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 74.1ns 
548394     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
550689     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.29s 
550689     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: indexOfSeqSingleton 
551455     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: indexOfSeqSingleton 
551459     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.82ms 
551460     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_indexOfSeqConcatFirst.proof 
551460     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 76.2ns 
551461     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
553756     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.3s 
553756     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: indexOfSeqConcatFirst 
554499     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: indexOfSeqConcatFirst 
554516     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 14.7ms 
554518     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_indexOfSeqConcatSecond.proof 
554518     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 83ns 
554519     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
556818     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.3s 
556818     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: indexOfSeqConcatSecond 
557584     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: indexOfSeqConcatSecond 
557601     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 14.13ms 
557602     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_indexOfSeqSub.proof 
557602     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 83.9ns 
557603     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
559908     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.3s 
559908     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: indexOfSeqSub 
560674     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: indexOfSeqSub 
560694     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 16.91ms 
560695     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfArray2seq.proof 
560695     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 72.8ns 
560696     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
562992     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.3s 
562992     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfArray2seq 
563756     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfArray2seq 
563759     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.3ms 
563760     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getAnyOfArray2seq.proof 
563760     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 65.1ns 
563761     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
566056     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.3s 
566056     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getAnyOfArray2seq 
566823     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getAnyOfArray2seq 
566827     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.24ms 
566828     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfArray2seq.proof 
566828     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 67.1ns 
566829     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
569119     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.29s 
569119     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfArray2seq 
569885     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfArray2seq 
569892     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 5.24ms 
569894     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_getAnyOfNPermInv.proof 
569894     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 98ns 
569894     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
572196     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.3s 
572196     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getAnyOfNPermInv 
572960     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getAnyOfNPermInv 
572967     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.54ms 
572968     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqNPermRange.proof 
572968     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 72.1ns 
572969     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
575262     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.29s 
575262     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqNPermRange 
576027     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqNPermRange 
576099     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 65.38ms 
576100     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermTrans.proof 
576100     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 89.9ns 
576101     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
578402     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.3s 
578402     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermTrans 
579168     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermTrans 
579196     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 23.9ms 
579197     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermRefl.proof 
579197     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 86ns 
579198     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
581495     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.3s 
581495     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermRefl 
582259     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermRefl 
582281     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 19.38ms 
582283     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermSplit.proof 
582283     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 86.4ns 
582283     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
584581     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.3s 
584581     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermSplit 
585347     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermSplit 
585349     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 306.4ns 
585351     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqNPermRight.proof 
585351     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 198.3ns 
585353     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
587684     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.33s 
587684     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqNPermRight 
588453     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqNPermRight 
588655     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 189.82ms 
588658     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermFromSwap.proof 
588658     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 168.8ns 
588659     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
590970     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.31s 
590970     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermFromSwap 
591743     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermFromSwap 
591795     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 46.56ms 
591796     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermTransAlt0.proof 
591796     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 74.1ns 
591797     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
594101     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.3s 
594101     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermTransAlt0 
594874     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermTransAlt0 
594877     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 380.5ns 
594880     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermTransAlt1.proof 
594880     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 223.6ns 
594881     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
597182     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.3s 
597182     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermTransAlt1 
597953     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermTransAlt1 
597957     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 400ns 
597959     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermTransAlt2.proof 
597959     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 221.5ns 
597960     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
600256     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.3s 
600256     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermTransAlt2 
601023     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermTransAlt2 
601025     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 395.5ns 
601027     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermTransAlt3.proof 
601027     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 67.3ns 
601028     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
603322     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.29s 
603322     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermTransAlt3 
604090     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermTransAlt3 
604092     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 541.1ns 
604093     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermForall.proof 
604093     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 73.8ns 
604094     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
606391     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.3s 
606391     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermForall 
607164     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermForall 
607256     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 90.26ms 
607259     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermExists.proof 
607259     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 256.1ns 
607260     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
609594     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.33s 
609594     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermExists 
610342     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermExists 
610420     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 76.29ms 
610422     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm2/Taclet_schiffl_lemma_2.proof 
610422     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 71.3ns 
610423     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
612750     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.33s 
612750     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: schiffl_lemma_2 
613520     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: schiffl_lemma_2 
613522     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.8ns 
613548     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 1: 'macro split-prop' 
613600     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 2: 'rule allRight' 
613616     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 3: 'rule allRight' 
613622     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 4: 'macro split-prop' 
613628     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 5: 'rule 'seqPermDefLeft'' 
613631     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 6: 'rule 'andLeft'' 
613631     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 7: 'rule 'exLeft'' 
613633     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 8: 'macro split-prop' 
613636     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 9: 'rule  seqNPermRange' 
613642     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 10: 'instantiate var=iv with='v_x_0' occ=1' 
613645     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 11: 'rule impLeft' 
613647     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 12: 'tryclose branch' 
613861     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 13: 'rule andLeft' 
613863     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 14: 'rule andLeft' 
613864     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 15: 'instantiate var=iv with='v_y_0' occ=1' 
613866     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 16: 'rule impLeft' 
613867     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 17: 'tryclose branch' 
613995     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 18: 'rule andLeft' 
613996     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 19: 'rule andLeft' 
614000     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 20: 'rule seqNPermDefLeft' 
614002     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 21: 'instantiate var=iv with='v_x_0' occ=2' 
614003     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 22: 'rule impLeft' 
614004     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 23: 'tryclose branch' 
614176     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 24: 'rule exLeft' 
614178     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 25: 'rule andLeft' 
614180     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 26: 'rule andLeft' 
614181     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 27: 'instantiate hide var=iv with='v_y_0' occ=2' 
614181     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 28: 'rule impLeft' 
614185     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 29: 'tryclose branch' 
614328     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 30: 'rule exLeft' 
614330     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 31: 'rule andLeft' 
614331     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 32: 'rule andLeft' 
614332     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 33: 'instantiate var=iv with='jv_0' occ=1' 
614333     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 34: 'rule impLeft' 
614334     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 35: 'tryclose branch' 
614343     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 36: 'rule andLeft' 
614344     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 37: 'rule andLeft' 
614345     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 38: 'rule castAdd formula='s_0[jv_0] = v_x_0' occ=0' 
614347     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 39: 'instantiate hide var=iv with='jv_1' occ=1' 
614349     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 40: 'rule impLeft' 
614351     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 41: 'tryclose branch' 
614360     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 42: 'rule andLeft' 
614361     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 43: 'rule andLeft' 
614363     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 44: 'rule castAdd formula='s_0[jv_1] = v_y_0' occ=0' 
614365     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 45: 'instantiate var=iv  with='v_x_0'' 
614365     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 46: 'rule impLeft' 
614367     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 47: 'tryclose branch' 
614517     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 48: 'instantiate var=iv  with='v_y_0'' 
614518     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 49: 'rule impLeft' 
614520     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 50: 'tryclose branch' 
614651     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 51: 'cut 'v_x_0 = v_y_0'' 
614652     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)'' 
614655     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 53: 'rule andRight' 
614656     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 54: 'rule andRight' 
614658     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 55: 'rule andRight' 
614659     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 56: 'rule andRight' 
614661     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 57: 'rule lenOfSwap' 
614663     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 58: 'tryclose branch' 
614668     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 59: 'rule seqNPermSwapNPerm' 
614670     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 60: 'instantiate hide var='iv' with='v_x_0' occ=1' 
614671     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 61: 'instantiate hide var='jv' with='jv_0'' 
614672     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 62: 'rule impLeft' 
614673     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 63: 'tryclose branch' 
614787     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 64: 'tryclose branch' 
614791     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 65: 'rule allRight' 
614793     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 66: 'rule impRight' 
614794     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 67: 'rule andLeft' 
614795     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 68: 'instantiate var=iv with='v_iv_0'' 
614796     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 69: 'rule impLeft' 
614798     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 70: 'tryclose branch' 
614933     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 71: 'rule getOfSwap' 
614935     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 72: 'rule ifthenelse_negated' 
614936     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 73: 'rule ifthenelse_split occ=0' 
614937     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 74: 'rule andLeft' 
614938     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 75: 'rule andLeft' 
614939     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 76: 'rule andLeft' 
614940     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 77: 'rule ifthenelse_split occ=0' 
614942     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 78: 'tryclose branch' 
615045     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 79: 'rule ifthenelse_split occ=0' 
615047     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 80: 'tryclose branch' 
615185     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 81: 'tryclose branch' 
615190     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 82: 'tryclose branch' 
615197     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 83: 'rule getOfSwap' 
615198     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 84: 'rule ifthenelse_negated' 
615199     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 85: 'rule ifthenelse_split occ=0' 
615201     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 86: 'rule andLeft' 
615203     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 87: 'rule andLeft' 
615204     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 88: 'rule andLeft' 
615204     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 89: 'rule ifthenelse_split occ=0' 
615206     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 90: 'tryclose branch' 
615216     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 91: 'tryclose branch' 
615222     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 92: 'tryclose branch' 
615351     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 93: 'rule getOfSwap' 
615353     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 94: 'rule ifthenelse_negated' 
615355     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 95: 'rule ifthenelse_split occ=0' 
615356     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 96: 'rule andLeft' 
615357     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 97: 'rule andLeft' 
615358     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 98: 'rule andLeft' 
615360     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 99: 'rule ifthenelse_split occ=0' 
615361     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 100: 'tryclose branch' 
615422     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 101: 'tryclose branch' 
615429     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 102: 'tryclose branch' 
615535     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 103: 'cut '(int)s_0[v_x_0] = (int)s_0[v_y_0]'' 
615537     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 104: 'rule seqNPermInjective' 
615539     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 105: 'instantiate hide var=iv with='v_x_0'' 
615540     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 106: 'instantiate hide var=jv with='v_y_0'' 
615541     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 107: 'rule impLeft' 
615543     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 108: 'tryclose branch' 
615706     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 109: 'tryclose branch' 
615711     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 110: 'cut '(int)s_0[v_x_0] = v_x_0'' 
615712     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)'' 
615714     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 112: 'rule andRight' 
615715     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 113: 'rule andRight' 
615716     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 114: 'rule andRight' 
615717     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 115: 'rule andRight' 
615717     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 116: 'tryclose branch' 
615729     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 117: 'rule seqNPermSwapNPerm' 
615730     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 118: 'instantiate hide var=iv with='v_y_0'' 
615731     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 119: 'instantiate hide var=jv with='jv_1'' 
615732     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 120: 'tryclose branch' 
615857     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 121: 'rule allRight' 
615859     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 122: 'rule impRight' 
615860     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 123: 'rule andLeft' 
615861     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 124: 'instantiate var=iv with='v_iv_0'' 
615862     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 125: 'rule impLeft' 
615863     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 126: 'tryclose branch' 
615976     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 127: 'rule getOfSwap' 
615977     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 128: 'rule ifthenelse_negated' 
615979     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 129: 'rule ifthenelse_split occ=0' 
615981     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 130: 'rule andLeft' 
615981     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 131: 'rule andLeft' 
615982     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 132: 'rule andLeft' 
615982     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 133: 'rule ifthenelse_split occ=0' 
615984     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 134: 'tryclose branch' 
616072     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 135: 'rule ifthenelse_split occ=0' 
616074     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 136: 'tryclose branch' 
616152     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 137: 'instantiate var=iv with='v_y_0'' 
616157     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 138: 'rule impLeft' 
616158     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 139: 'tryclose branch' 
616163     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 140: 'tryclose branch' 
616168     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 141: 'tryclose branch' 
616172     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 142: 'tryclose branch' 
616332     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 143: 'rule getOfSwap' 
616334     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 144: 'rule ifthenelse_negated' 
616335     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 145: 'rule ifthenelse_split occ=0' 
616336     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 146: 'tryclose branch' 
616347     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 147: 'tryclose branch' 
616431     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 148: 'tryclose branch' 
619986     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 149: 'cut  '(int)s_0[v_y_0] = v_y_0'' 
619988     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)'' 
619993     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 151: 'rule andRight' 
619999     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 152: 'rule andRight' 
620000     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 153: 'rule andRight' 
620000     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 154: 'rule andRight' 
620001     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 155: 'tryclose branch' 
620009     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 156: 'rule seqNPermSwapNPerm' 
620011     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 157: 'instantiate hide var=iv with='v_x_0'' 
620012     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 158: 'instantiate hide var=jv with='jv_0'' 
620012     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 159: 'rule impLeft' 
620013     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 160: 'tryclose branch' 
620107     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 161: 'tryclose branch' 
620111     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 162: 'rule allRight' 
620113     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 163: 'rule impRight' 
620113     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 164: 'rule andLeft' 
620114     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 165: 'instantiate var=iv with='v_iv_0'' 
620116     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 166: 'rule impLeft' 
620116     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 167: 'tryclose branch' 
620212     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 168: 'rule getOfSwap' 
620214     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 169: 'rule ifthenelse_negated' 
620215     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 170: 'rule ifthenelse_split occ=0' 
620216     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 171: 'rule andLeft' 
620216     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 172: 'rule andLeft' 
620217     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 173: 'rule andLeft' 
620218     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 174: 'rule ifthenelse_split occ=0' 
620219     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 175: 'tryclose branch' 
620296     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 176: 'rule ifthenelse_split occ=0' 
620298     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 177: 'tryclose branch' 
620377     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 178: 'tryclose branch' 
620382     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 179: 'tryclose branch' 
620387     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 180: 'rule getOfSwap' 
620388     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 181: 'rule ifthenelse_negated' 
620389     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 182: 'rule ifthenelse_split occ=0' 
620390     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 183: 'tryclose branch' 
620401     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 184: 'tryclose branch' 
620539     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 185: 'rule getOfSwap' 
620540     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 186: 'rule ifthenelse_negated' 
620541     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 187: 'rule ifthenelse_split occ=0' 
620542     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 188: 'tryclose branch' 
620615     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 189: 'tryclose branch' 
620625     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 190: 'cut '(int)s_0[v_x_0]=v_y_0'' 
620626     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)'' 
620628     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 192: 'rule andRight' 
620629     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 193: 'rule andRight' 
620629     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 194: 'rule andRight' 
620630     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 195: 'rule andRight' 
620631     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 196: 'tryclose branch' 
620642     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 197: 'rule seqNPermSwapNPerm' 
620643     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 198: 'instantiate hide var=iv with='jv_0'' 
620644     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 199: 'instantiate hide var=jv with='v_x_0'' 
620645     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 200: 'rule impLeft' 
620646     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 201: 'tryclose branch' 
620734     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 202: 'rule seqNPermSwapNPerm formula='seqNPerm(seqSwap(s_0, jv_0, v_x_0))'' 
620736     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 203: 'instantiate hide var=iv with='jv_0'' 
620737     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 204: 'instantiate hide var=jv with='v_y_0'' 
620738     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 205: 'rule impLeft' 
620739     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 206: 'tryclose branch' 
620829     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 207: 'tryclose branch' 
620834     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 208: 'rule allRight' 
620835     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 209: 'rule impRight' 
620836     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 210: 'rule andLeft' 
620836     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 211: 'instantiate var=iv with='v_iv_0'' 
620837     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 212: 'rule impLeft' 
620838     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 213: 'tryclose branch' 
620936     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 214: 'rule getOfSwap' 
620937     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 215: 'rule ifthenelse_negated' 
620938     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 216: 'rule ifthenelse_split occ=0' 
620939     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 217: 'rule andLeft' 
620940     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 218: 'rule andLeft' 
620940     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 219: 'rule andLeft' 
620941     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 220: 'rule ifthenelse_split occ=0' 
620942     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 221: 'rule getOfSwap' 
620943     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 222: 'rule ifthenelse_negated' 
620943     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 223: 'rule ifthenelse_split occ=0' 
620945     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 224: 'rule andLeft' 
620945     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 225: 'rule andLeft' 
620946     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 226: 'rule andLeft' 
620946     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 227: 'rule ifthenelse_split occ=0' 
620947     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 228: 'tryclose branch' 
621034     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 229: 'rule ifthenelse_split occ=0' 
621035     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 230: 'tryclose branch' 
621041     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 231: 'tryclose branch' 
621118     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 232: 'tryclose branch' 
621197     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 233: 'rule ifthenelse_split' 
621198     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 234: 'rule getOfSwap' 
621199     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 235: 'rule ifthenelse_negated' 
621200     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 236: 'rule ifthenelse_split occ=0' 
621200     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 237: 'rule andLeft' 
621201     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 238: 'rule andLeft' 
621201     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 239: 'rule andLeft' 
621201     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 240: 'rule ifthenelse_split occ=0' 
621202     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 241: 'tryclose branch' 
621287     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 242: 'tryclose branch' 
621293     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 243: 'tryclose branch' 
621383     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 244: 'rule getOfSwap' 
621384     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 245: 'rule ifthenelse_negated' 
621385     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 246: 'rule ifthenelse_split occ=0' 
621386     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 247: 'rule andLeft' 
621386     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 248: 'rule andLeft' 
621386     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 249: 'rule andLeft' 
621387     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 250: 'rule ifthenelse_split occ=0' 
621387     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 251: 'tryclose branch' 
621393     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 252: 'rule ifthenelse_split occ=0' 
621393     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 253: 'tryclose branch' 
621473     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 254: 'tryclose branch' 
621479     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 255: 'tryclose branch' 
621485     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 256: 'tryclose branch' 
621584     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 257: 'rule getOfSwap' 
621585     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 258: 'rule ifthenelse_negated' 
621586     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 259: 'rule ifthenelse_split occ=0' 
621587     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 260: 'rule andLeft' 
621587     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 261: 'rule andLeft' 
621588     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 262: 'rule andLeft' 
621588     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 263: 'rule ifthenelse_split occ=0' 
621589     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 264: 'tryclose branch' 
621644     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 265: 'rule ifthenelse_split occ=0' 
621645     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 266: 'rule getOfSwap' 
621646     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 267: 'rule ifthenelse_negated' 
621646     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 268: 'rule ifthenelse_split occ=0' 
621647     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 269: 'tryclose branch' 
621653     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 270: 'tryclose branch' 
621659     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 271: 'tryclose branch' 
621775     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 272: 'tryclose branch' 
621864     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 273: 'rule getOfSwap' 
621865     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 274: 'rule ifthenelse_negated' 
621866     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 275: 'rule ifthenelse_split occ=0' 
621867     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 276: 'tryclose branch' 
622035     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 277: 'tryclose branch' 
622124     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 278: 'cut 'int::seqGet(s_0, v_y_0)=v_x_0'' 
622125     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 279: 'tryclose branch' 
625265     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 280: 'rule seqNPermSwapNPerm' 
625270     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 281: 'instantiate hide var=iv with='jv_1'' 
625271     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 282: 'instantiate hide var=jv with='v_y_0'' 
625272     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 283: 'rule impLeft' 
625272     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 284: 'tryclose branch' 
625387     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 285: 'rule seqNPermSwapNPerm formula='seqNPerm(seqSwap(s_0,jv_1,v_y_0))'' 
625388     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 286: 'instantiate hide var=iv with='jv_1'' 
625389     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 287: 'instantiate hide var=jv with='v_x_0'' 
625390     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 288: 'rule impLeft' 
625391     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 289: 'tryclose branch' 
625497     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 290: 'tryclose branch' 
628565     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 291: 'tryclose branch' 
631803     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 292: 'rule seqNPermSwapNPerm formula='seqNPerm(s_0)'' 
631807     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 293: 'instantiate hide var=iv with='v_x_0'' 
631808     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 294: 'instantiate hide var=jv with='jv_0'' 
631809     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 295: 'rule impLeft' 
631809     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 296: 'tryclose branch' 
631923     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 297: 'rule seqNPermSwapNPerm formula='seqNPerm(seqSwap(s_0,v_x_0,jv_0))'' 
631924     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 298: 'instantiate hide var=iv with='v_y_0'' 
631925     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 299: 'instantiate hide var=jv with='jv_1'' 
631926     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)' ...' 
631927     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 301: 'tryclose branch' 
633099     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm2/Taclet_schiffl_thm_1.proof 
633099     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 94.8ns 
633100     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
635474     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.37s 
635474     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: schiffl_thm_1 
636266     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: schiffl_thm_1 
636268     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 9.1ns 
636268     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 1: 'macro split-prop' 
636278     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 2: 'rule schiffl_lemma_2 formula='seqPerm(f_s, f_t)'' 
636289     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 3: 'instantiate hide var=x with='f_x'' 
636292     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 4: 'instantiate hide var=y with='f_y'' 
636294     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 5: 'rule impLeft' 
636294     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 6: 'tryclose branch' 
636299     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 7: 'rule exLeft' 
636300     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 8: 'macro split-prop' 
636304     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 9: 'rule seqPermDef occ=1' 
636307     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 10: 'rule andRight' 
636307     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 11: 'tryclose branch' 
636317     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 12: 'instantiate hide var=s with='r_0'' 
636319     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 13: 'rule andRight' 
636320     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 14: 'tryclose branch' 
636368     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 15: 'rule allRight' 
636369     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 16: 'rule impRight' 
636369     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 17: 'instantiate hide var=iv with='iv_0'' 
636370     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 18: 'rule impLeft' 
636371     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 19: 'tryclose branch' 
636440     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 20: 'rule andLeft' 
636440     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 21: 'rule seqNPermRange' 
636441     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 22: 'instantiate hide var=iv with='iv_0'' 
636442     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 23: 'rule impLeft' 
636443     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 24: 'tryclose branch' 
636447     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 25: 'rule andLeft' 
636448     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 26: 'rule andLeft' 
636448     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 27: 'rule seqNPermRange' 
636449     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 28: 'instantiate hide var=iv with='f_x'' 
636449     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 29: 'rule impLeft' 
636450     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 30: 'tryclose branch' 
636529     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 31: 'rule andLeft' 
636530     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 32: 'rule andLeft' 
636531     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 33: 'rule seqNPermRange' 
636532     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 34: 'instantiate hide var=iv with='f_y'' 
636533     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 35: 'rule impLeft' 
636533     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 36: 'tryclose branch' 
636612     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 37: 'rule andLeft' 
636613     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 38: 'rule andLeft' 
636614     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 39: 'rule getOfSeqDef occ=0' 
636614     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 40: 'rule getOfSeqDef' 
636615     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 41: 'rule ifthenelse_split occ=0' 
636616     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 42: 'rule andLeft occ=0' 
636616     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 43: 'rule sub_zero_2 occ=0' 
636617     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 44: 'rule ifthenelse_split occ=2' 
636617     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 45: 'rule andLeft' 
636618     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 46: 'rule sub_zero_2 occ=0' 
636618     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 47: 'rule add_zero_right occ=0' 
636619     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 48: 'rule add_zero_right occ=0' 
636619     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 49: 'rule add_zero_right occ=0' 
636620     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 50: 'rule add_zero_right occ=0' 
636620     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 51: 'rule add_zero_right occ=0' 
636621     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 52: 'rule add_zero_right occ=0' 
636621     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 53: 'rule ifthenelse_split occ=0' 
636622     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 54: 'rule ifthenelse_split occ=0' 
636623     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 55: 'tryclose branch' 
636626     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 56: 'tryclose branch' 
636656     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 57: 'rule ifthenelse_split occ=0' 
636658     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 58: 'tryclose branch' 
636703     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 59: 'rule ifthenelse_split occ=0' 
636705     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 60: 'rule seqNPermInjective' 
636706     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 61: 'instantiate hide var=iv with='iv_0'' 
636708     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 62: 'instantiate hide var=jv with='f_y'' 
636709     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 63: 'rule impLeft' 
636710     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 64: 'tryclose branch' 
636752     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 65: 'tryclose branch' 
636754     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 66: 'rule ifthenelse_split occ=0' 
636756     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 67: 'rule seqNPermInjective' 
636757     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 68: 'instantiate hide var=iv with='iv_0'' 
636759     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 69: 'instantiate hide var=jv with='f_x'' 
636759     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 70: 'rule impLeft' 
636760     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 71: 'tryclose branch' 
636802     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 72: 'tryclose branch' 
636805     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 73: 'tryclose branch' 
636808     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 74: 'tryclose branch' 
636859     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 75: 'tryclose branch' 
636912     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_eqSameSeq.proof 
636913     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 87.8ns 
636913     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
639324     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.41s 
639324     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: eqSameSeq 
640144     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: eqSameSeq 
640175     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 27.44ms