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

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

tests
0

failures
0

ignored
10m36.48s

duration
100%

successful

Tests

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

Standard output

358        INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src/test/resources/testcase/dummyTrue.key 
382        DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 10.42ms 
584        INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
596        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)

1511       DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for Meta 
1514       DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for Meta 
1517       DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for Meta 
1517       DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for Meta 
2919       DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for JavaBigintExpression 
8090       DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 7.51s 
8147       INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof dummyTrue.key 
8177       DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 31.5ns 
8191       INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/firstOrder/Taclet_eqTermCut.proof 
8192       DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 181.1ns 
8206       INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
10989      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.78s 
10991      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: eqTermCut 
11919      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: eqTermCut 
11941      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 16.69ms 
11950      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/firstOrder/Taclet_equivAllRight.proof 
11950      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 233ns 
11951      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
14458      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.51s 
14463      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: equivAllRight 
15337      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: equivAllRight 
15351      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 10.51ms 
15353      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_irrflConcrete1.proof 
15353      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 198.7ns 
15354      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
17925      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.57s 
17926      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: irrflConcrete1 
18717      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: irrflConcrete1 
18725      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.26ms 
18728      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_irrflConcrete2.proof 
18728      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 132.7ns 
18729      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
21190      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.46s 
21190      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: irrflConcrete2 
22004      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: irrflConcrete2 
22019      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 11.06ms 
22022      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_cancel_gtPos.proof 
22023      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 133.4ns 
22024      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
24450      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.43s 
24450      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: cancel_gtPos 
25275      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: cancel_gtPos 
25315      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 36.76ms 
25317      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_cancel_gtNeg.proof 
25318      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 175.5ns 
25319      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
27741      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.42s 
27741      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: cancel_gtNeg 
28560      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: cancel_gtNeg 
28580      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 16.6ms 
28582      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intRulesIgnoringOF/Taclet_moduloIntIsInInt.proof 
28583      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 290.9ns 
28584      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
30979      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.4s 
30980      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: moduloIntIsInInt 
31811      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: moduloIntIsInInt 
31814      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 698.9ns 
31816      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intRulesIgnoringOF/Taclet_moduloLongIsInLong.proof 
31816      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 208.6ns 
31817      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
34193      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.38s 
34194      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: moduloLongIsInLong 
34977      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: moduloLongIsInLong 
34980      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 540.3ns 
34982      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intRulesIgnoringOF/Taclet_moduloShortIsInShort.proof 
34982      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 302.4ns 
34983      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
37337      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.35s 
37338      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: moduloShortIsInShort 
38113      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: moduloShortIsInShort 
38116      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 558.3ns 
38118      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intRulesIgnoringOF/Taclet_moduloByteIsInByte.proof 
38118      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 302ns 
38119      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
40467      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.35s 
40467      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: moduloByteIsInByte 
41251      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: moduloByteIsInByte 
41254      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 589.1ns 
41256      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intRulesIgnoringOF/Taclet_moduloCharIsInChar.proof 
41257      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 337.4ns 
41258      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
43610      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.35s 
43611      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: moduloCharIsInChar 
44384      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: moduloCharIsInChar 
44387      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 534.3ns 
44390      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_div_unique1.proof 
44390      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 326.4ns 
44392      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
46861      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.47s 
46862      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: div_unique1 
47611      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: div_unique1 
47653      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 37.28ms 
47658      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_div_unique2.proof 
47658      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 461.4ns 
47660      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
50023      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.36s 
50023      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: div_unique2 
50772      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: div_unique2 
50813      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 37.39ms 
50818      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_div_exists.proof 
50818      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 313.9ns 
50820      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
53180      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.36s 
53180      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: div_exists 
53926      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: div_exists 
54100      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 164.74ms 
54103      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_div_one.proof 
54103      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 121.4ns 
54104      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
56469      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.36s 
56469      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: div_one 
57253      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: div_one 
57259      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.69ms 
57263      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdiv_one.proof 
57263      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 306.6ns 
57264      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
59609      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.34s 
59609      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdiv_one 
60387      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdiv_one 
60389      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.18ms 
60393      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_div_zero.proof 
60393      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 496.1ns 
60395      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
62731      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.34s 
62731      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: div_zero 
63500      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: div_zero 
63541      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 36.52ms 
63544      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divResZero1.proof 
63545      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 309.7ns 
63546      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
65895      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.35s 
65896      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divResZero1 
66666      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divResZero1 
66680      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 11.58ms 
66682      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divResZero2.proof 
66682      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 173.9ns 
66683      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
69010      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.33s 
69010      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divResZero2 
69792      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divResZero2 
69805      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 10.57ms 
69806      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divResOne1.proof 
69807      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 98.9ns 
69807      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
72151      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.34s 
72152      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divResOne1 
72922      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divResOne1 
72938      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 12.9ms 
72940      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divResOne2.proof 
72941      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 327.4ns 
72942      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
75304      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.36s 
75304      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divResOne2 
76075      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divResOne2 
76089      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 11.4ms 
76091      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_div_cancel1.proof 
76092      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 284.2ns 
76093      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
78430      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.34s 
78430      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: div_cancel1 
79195      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: div_cancel1 
79219      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 20.41ms 
79220      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_div_cancel2.proof 
79220      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 114.5ns 
79221      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
81576      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.35s 
81578      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: div_cancel2 
82330      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: div_cancel2 
82333      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.07ms 
82336      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divAddMultDenom.proof 
82336      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 280.1ns 
82337      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
84682      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.35s 
84683      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divAddMultDenom 
85426      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divAddMultDenom 
85465      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 33.21ms 
85468      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divMinus.proof 
85468      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 318ns 
85469      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
87821      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.35s 
87821      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divMinus 
88605      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divMinus 
88672      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 59.78ms 
88679      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divMinusDenom.proof 
88680      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 551.3ns 
88681      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
91023      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.34s 
91023      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divMinusDenom 
91785      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divMinusDenom 
91828      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 37.52ms 
91830      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divLeastDPos.proof 
91830      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 106.1ns 
91831      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
94157      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.33s 
94159      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divLeastDPos 
94919      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divLeastDPos 
94927      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 5.07ms 
94930      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divLeastDNeg.proof 
94931      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 635.1ns 
94932      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
97255      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.32s 
97256      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divLeastDNeg 
98014      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divLeastDNeg 
98026      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 9.6ms 
98027      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divGreatestDPos.proof 
98027      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 80.4ns 
98028      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
100358     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.33s 
100358     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divGreatestDPos 
101162     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divGreatestDPos 
101173     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 8.11ms 
101175     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divGreatestDNeg.proof 
101175     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 154.4ns 
101176     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
103521     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.35s 
103521     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divGreatestDNeg 
104291     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divGreatestDNeg 
104298     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 5.03ms 
104299     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divIncreasingPos.proof 
104299     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 91ns 
104300     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
106630     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.33s 
106631     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divIncreasingPos 
107398     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divIncreasingPos 
107405     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 5.02ms 
107408     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divIncreasingNeg.proof 
107408     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 316.7ns 
107409     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
109727     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.32s 
109727     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divIncreasingNeg 
110486     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divIncreasingNeg 
110492     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.52ms 
110493     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdiv_zero.proof 
110493     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 83.5ns 
110494     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
112853     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.36s 
112854     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdiv_zero 
113590     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdiv_zero 
113594     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.25ms 
113595     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdivPulloutMinusNum.proof 
113595     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 76.5ns 
113596     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
115942     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.35s 
115942     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdivPulloutMinusNum 
116680     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdivPulloutMinusNum 
116690     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 7.73ms 
116691     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdivPulloutMinusDenom.proof 
116691     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 92.2ns 
116692     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
119032     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.34s 
119032     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdivPulloutMinusDenom 
119779     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdivPulloutMinusDenom 
119857     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 71.62ms 
119858     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdiv_uniquePosPos.proof 
119858     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 92.3ns 
119859     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
122176     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.32s 
122177     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdiv_uniquePosPos 
122938     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdiv_uniquePosPos 
122956     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 13.9ms 
122961     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdiv_uniquePosNeg.proof 
122961     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 348.3ns 
122962     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
125286     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.32s 
125286     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdiv_uniquePosNeg 
126045     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdiv_uniquePosNeg 
126062     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 13.79ms 
126063     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdiv_uniqueNegPos.proof 
126063     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 100.2ns 
126064     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
128474     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.41s 
128475     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdiv_uniqueNegPos 
129234     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdiv_uniqueNegPos 
129251     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 13.95ms 
129254     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdiv_uniqueNegNeg.proof 
129254     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 271.9ns 
129255     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
131570     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.32s 
131571     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdiv_uniqueNegNeg 
132336     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdiv_uniqueNegNeg 
132352     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 13.27ms 
132353     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdivMultDenom1.proof 
132353     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 92.7ns 
132354     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
134675     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.32s 
134675     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdivMultDenom1 
135435     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdivMultDenom1 
135476     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 35.41ms 
135477     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdivMultDenom2.proof 
135477     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 96.3ns 
135478     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
137791     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.31s 
137792     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdivMultDenom2 
138568     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdivMultDenom2 
138575     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.58ms 
138578     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_mod_geZero.proof 
138578     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 86.6ns 
138579     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
140907     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.33s 
140907     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: mod_geZero 
141664     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: mod_geZero 
141668     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.43ms 
141669     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_mod_lessDenom.proof 
141669     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 71.5ns 
141670     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
144007     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.34s 
144007     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: mod_lessDenom 
144744     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: mod_lessDenom 
144752     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 6.02ms 
144753     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmod_NumPos.proof 
144753     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 85.2ns 
144754     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
147091     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.34s 
147091     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmod_NumPos 
147827     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmod_NumPos 
147835     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 5.73ms 
147836     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmod_NumNeg.proof 
147836     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 86ns 
147837     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
150177     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.34s 
150177     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmod_NumNeg 
150919     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmod_NumNeg 
150947     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 25.37ms 
150948     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmod_geZero.proof 
150948     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 87.2ns 
150949     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
153292     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.34s 
153292     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmod_geZero 
154053     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmod_geZero 
154060     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 5.53ms 
154062     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmodNumZero.proof 
154062     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 89.5ns 
154062     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
156381     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.32s 
156381     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmodNumZero 
157142     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmodNumZero 
157145     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.16ms 
157146     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmod_pulloutminusNum.proof 
157146     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 73.3ns 
157147     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
159471     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.32s 
159472     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmod_pulloutminusNum 
160238     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmod_pulloutminusNum 
160241     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.75ms 
160242     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmod_pulloutminusDenom.proof 
160243     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 82.4ns 
160243     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
162556     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.31s 
162556     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmod_pulloutminusDenom 
163320     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmod_pulloutminusDenom 
163324     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.06ms 
163326     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmodUnique1.proof 
163326     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 235.7ns 
163327     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
165642     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.31s 
165642     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmodUnique1 
166401     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmodUnique1 
166469     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 58.74ms 
166470     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmodUnique2.proof 
166470     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 99.3ns 
166471     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
168832     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.36s 
168833     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmodUnique2 
169630     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmodUnique2 
169710     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 69.62ms 
169712     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_intDivRem.proof 
169712     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 113.3ns 
169713     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
172149     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.44s 
172149     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: intDivRem 
172946     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: intDivRem 
172950     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.71ms 
172951     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmodjmod.proof 
172951     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 84.4ns 
172952     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
175308     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.36s 
175308     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmodjmod 
176043     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmodjmod 
176076     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 29.9ms 
176078     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmodDivisible.proof 
176078     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 275.4ns 
176079     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
178404     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.32s 
178405     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmodDivisible 
179146     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmodDivisible 
179174     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 25.07ms 
179175     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmodDivisibleRep.proof 
179176     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 78.8ns 
179176     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
181513     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.34s 
181513     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmodDivisibleRep 
182255     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmodDivisibleRep 
182260     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.16ms 
182267     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdivAddMultDenom.proof 
182267     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 258.7ns 
182268     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
184669     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.4s 
184669     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdivAddMultDenom 
185424     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdivAddMultDenom 
185564     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 126.95ms 
185566     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmodAltZero.proof 
185566     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 227.5ns 
185567     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
187896     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.33s 
187896     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmodAltZero 
188658     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmodAltZero 
188673     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 12.32ms 
188674     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmodAddMultDenomZero.proof 
188674     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 79ns 
188676     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
191006     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.33s 
191007     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmodAddMultDenomZero 
191771     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmodAddMultDenomZero 
191778     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 5.83ms 
191779     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_polyDiv_zero.proof 
191780     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 74.1ns 
191780     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
194092     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.31s 
194092     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: polyDiv_zero 
194853     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: polyDiv_zero 
194878     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 21.34ms 
194880     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_polyMod_ltdivDenom.proof 
194880     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 79.9ns 
194881     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
197200     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.32s 
197200     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: polyMod_ltdivDenom 
197957     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: polyMod_ltdivDenom 
197968     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 5.83ms 
197971     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_empty.proof 
197971     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 208.5ns 
197972     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
200278     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.31s 
200279     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_empty 
201029     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_empty 
201032     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.51ms 
201034     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_induction_upper.proof 
201034     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 116.4ns 
201035     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
203338     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.3s 
203338     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_upper 
204094     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_induction_upper 
204098     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.82ms 
204099     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_induction_lower.proof 
204099     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 67.9ns 
204100     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
206427     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.33s 
206427     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_lower 
207164     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_induction_lower 
207186     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 19.11ms 
207187     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_bounds.proof 
207187     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 68ns 
207188     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
209531     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.34s 
209531     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_bounds 
210270     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_bounds 
210286     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 13.43ms 
210288     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_bounds2.proof 
210288     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 78.2ns 
210289     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
212649     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.36s 
212649     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_bounds2 
213392     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_bounds2 
213407     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 12.55ms 
213408     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_induction_upper2.proof 
213408     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 70.8ns 
213409     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
215750     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.34s 
215750     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_upper2 
216506     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_induction_upper2 
216509     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.58ms 
216510     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_induction_upper_concrete.proof 
216510     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 77.8ns 
216511     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
218832     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.32s 
218832     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_upper_concrete 
219588     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_induction_upper_concrete 
219593     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.73ms 
219594     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_induction_upper_concrete_2.proof 
219594     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 88.2ns 
219594     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
221909     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.31s 
221909     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_upper_concrete_2 
222665     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_induction_upper_concrete_2 
222671     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.66ms 
222672     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_induction_upper2_concrete.proof 
222672     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 87.7ns 
222673     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
224989     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.32s 
224990     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_upper2_concrete 
225745     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_induction_upper2_concrete 
225748     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.33ms 
225749     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_induction_lower_concrete.proof 
225749     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 73.8ns 
225750     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
228059     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.31s 
228060     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_lower_concrete 
228817     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_induction_lower_concrete 
228819     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 670.8ns 
228820     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_induction_lower2.proof 
228820     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 65.4ns 
228821     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
231132     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.31s 
231132     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_lower2 
231889     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_induction_lower2 
231893     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.28ms 
231894     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_induction_lower2_concrete.proof 
231894     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 85.7ns 
231895     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
234200     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.31s 
234201     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_lower2_concrete 
234958     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_induction_lower2_concrete 
234960     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1ms 
234962     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_positive.proof 
234962     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 57.2ns 
234962     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
237268     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.31s 
237268     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_positive 
238023     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_positive 
238069     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 42.6ms 
238070     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_upper_bound.proof 
238070     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 74.4ns 
238071     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
240409     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.34s 
240409     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_upper_bound 
241152     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_upper_bound 
241193     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 37.42ms 
241194     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_lower_bound.proof 
241194     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 69.6ns 
241195     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
243528     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.33s 
243529     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_lower_bound 
244263     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_lower_bound 
244294     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 28.44ms 
244296     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_positive_lower_bound_element.proof 
244296     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 72ns 
244296     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
246634     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.34s 
246634     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_positive_lower_bound_element 
247398     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_positive_lower_bound_element 
247442     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 39.55ms 
247445     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_sub_same_index.proof 
247445     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 218.3ns 
247446     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
249758     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.31s 
249758     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_sub_same_index 
250513     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_sub_same_index 
250543     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 26.24ms 
250544     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_less_same_index.proof 
250544     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 84.3ns 
250545     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
252856     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.31s 
252856     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_less_same_index 
253611     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_less_same_index 
253661     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 45.53ms 
253662     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_equal_except_one_index.proof 
253662     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 73.5ns 
253663     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
255979     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.32s 
255980     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_equal_except_one_index 
256734     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_equal_except_one_index 
256761     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 23.6ms 
256762     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_is_max.proof 
256762     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 69.1ns 
256763     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
259086     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.32s 
259087     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_is_max 
259850     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_is_max 
259870     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 17.12ms 
259871     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_is_max2.proof 
259871     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 73.4ns 
259872     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
262199     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.33s 
262200     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_is_max2 
262956     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_is_max2 
262979     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 20.63ms 
262981     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_is_max3.proof 
262981     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 67ns 
262981     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
265290     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.31s 
265291     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_is_max3 
266045     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_is_max3 
266065     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 16.26ms 
266066     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_is_max4.proof 
266066     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 61.4ns 
266067     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
268392     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.33s 
268393     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_is_max4 
269126     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_is_max4 
269153     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 23.71ms 
269154     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_lt_max.proof 
269154     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 69ns 
269155     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
271478     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.32s 
271478     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_lt_max 
272213     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_lt_max 
272237     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 21.67ms 
272239     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_lt_max2.proof 
272239     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 75.6ns 
272239     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
274577     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.34s 
274577     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_lt_max2 
275314     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_lt_max2 
275339     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 21.64ms 
275341     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_lt_max3.proof 
275341     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 75ns 
275342     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
277677     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.34s 
277677     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_lt_max3 
278433     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_lt_max3 
278458     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 21.22ms 
278459     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_lt_max4.proof 
278459     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 79.2ns 
278460     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
280777     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.32s 
280777     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_lt_max4 
281533     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_lt_max4 
281553     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 17.77ms 
281554     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_gt0.proof 
281554     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 73.2ns 
281555     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
283867     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.31s 
283867     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_gt0 
284624     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_gt0 
284648     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 21.54ms 
284649     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_gt0_alt.proof 
284649     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 70.4ns 
284650     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
286956     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.31s 
286956     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_gt0_alt 
287712     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_gt0_alt 
287736     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 21.51ms 
287737     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_add_concrete.proof 
287737     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 75.3ns 
287738     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
290044     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.31s 
290044     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_add_concrete 
290802     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_add_concrete 
290809     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 5.53ms 
290810     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bprod/Taclet_bprod_all_positive.proof 
290810     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 58.5ns 
290811     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
293122     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.31s 
293122     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bprod_all_positive 
293879     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bprod_all_positive 
293896     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 14.46ms 
293897     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bprod/Taclet_bprod_split.proof 
293897     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 56.5ns 
293898     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
296202     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.3s 
296202     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bprod_split 
296961     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bprod_split 
296965     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.88ms 
296966     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powConcrete0.proof 
296966     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 60.5ns 
296967     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
299291     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.32s 
299292     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powConcrete0 
300029     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powConcrete0 
300031     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 563.7ns 
300032     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powConcrete1.proof 
300032     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 59.6ns 
300033     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
302357     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.32s 
302357     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powConcrete1 
303096     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powConcrete1 
303099     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 717ns 
303100     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powSplitFactor.proof 
303101     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 168.6ns 
303101     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
305424     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.32s 
305424     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powSplitFactor 
306158     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powSplitFactor 
306166     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.61ms 
306167     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powAdd.proof 
306167     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 60.5ns 
306168     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
308488     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.32s 
308488     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powAdd 
309243     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powAdd 
309249     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.02ms 
309250     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powMono.proof 
309250     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 61.4ns 
309251     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
311557     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.31s 
311557     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powMono 
312311     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powMono 
312323     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 9.55ms 
312324     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powMonoConcrete.proof 
312324     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 67.1ns 
312325     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
314631     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.31s 
314632     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powMonoConcrete 
315390     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powMonoConcrete 
315394     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.95ms 
315395     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powMonoConcreteRight.proof 
315395     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 51.1ns 
315396     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
317702     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.31s 
317703     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powMonoConcreteRight 
318456     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powMonoConcreteRight 
318458     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 528.3ns 
318459     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powPositive.proof 
318459     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 50.5ns 
318460     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
320763     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.3s 
320763     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powPositive 
321521     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powPositive 
321529     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.57ms 
321531     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powPositiveConcrete.proof 
321531     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 166.8ns 
321531     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
323831     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.3s 
323831     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powPositiveConcrete 
324584     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powPositiveConcrete 
324586     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 671.4ns 
324588     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powGeq1Concrete.proof 
324588     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 50.7ns 
324588     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
326891     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.3s 
326891     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powGeq1Concrete 
327651     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powGeq1Concrete 
327653     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 533.7ns 
327654     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_pow2InIntLower.proof 
327654     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 67ns 
327655     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
329962     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.31s 
329962     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: pow2InIntLower 
330721     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: pow2InIntLower 
330722     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 577.5ns 
330723     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_pow2InIntUpper.proof 
330724     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 60.8ns 
330724     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
333043     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.32s 
333043     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: pow2InIntUpper 
333779     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: pow2InIntUpper 
333782     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.84ms 
333783     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logSelfConcrete.proof 
333783     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 49.6ns 
333784     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
336099     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.32s 
336099     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logSelfConcrete 
336834     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logSelfConcrete 
336842     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 6.52ms 
336843     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_log1Concrete.proof 
336843     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 58.3ns 
336844     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
339170     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.33s 
339170     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: log1Concrete 
339907     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: log1Concrete 
339910     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.18ms 
339911     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logProduct.proof 
339911     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 60.4ns 
339912     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
342233     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.32s 
342233     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logProduct 
342990     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logProduct 
342996     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.88ms 
342997     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logTimesBaseConcrete.proof 
342997     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 53ns 
342998     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
345304     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.31s 
345304     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logTimesBaseConcrete 
346061     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logTimesBaseConcrete 
346065     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.21ms 
346066     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logProdIdentity.proof 
346066     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 59.8ns 
346067     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
348372     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.3s 
348372     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logProdIdentity 
349129     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logProdIdentity 
349144     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 12.27ms 
349145     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logProdIdentityConcrete.proof 
349145     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 59.2ns 
349146     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
351457     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.31s 
351457     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logProdIdentityConcrete 
352220     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logProdIdentityConcrete 
352223     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.72ms 
352224     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logPowIdentity.proof 
352224     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 54.7ns 
352225     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
354526     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.3s 
354526     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logPowIdentity 
355284     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logPowIdentity 
355287     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.53ms 
355289     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logPowIdentityConcrete.proof 
355289     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 165.6ns 
355290     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
357598     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.31s 
357598     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logPowIdentityConcrete 
358356     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logPowIdentityConcrete 
358360     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.9ms 
358361     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logPositive.proof 
358361     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 48ns 
358361     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
360667     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.31s 
360668     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logPositive 
361426     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logPositive 
361445     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 16.35ms 
361447     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logPositiveConcrete.proof 
361448     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 201.7ns 
361448     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
363788     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.34s 
363788     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logPositiveConcrete 
364526     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logPositiveConcrete 
364530     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 518.9ns 
364532     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logMono.proof 
364532     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 57.7ns 
364532     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
366851     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.32s 
366851     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logMono 
367589     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logMono 
367628     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 34.4ms 
367629     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logMonoConcrete.proof 
367629     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 56.8ns 
367630     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
369959     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.33s 
369959     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logMonoConcrete 
370696     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logMonoConcrete 
370699     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.68ms 
370700     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powLogLess.proof 
370700     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 48.4ns 
370701     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
373021     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.32s 
373021     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powLogLess 
373781     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powLogLess 
373801     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 17.85ms 
373803     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powLogMore2.proof 
373803     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 58.1ns 
373804     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
376112     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.31s 
376112     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powLogMore2 
376885     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powLogMore2 
376905     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 17.46ms 
376906     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logLessThanPow.proof 
376906     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 54.9ns 
376907     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
379310     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.4s 
379310     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logLessThanPow 
380070     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logLessThanPow 
380093     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 19.89ms 
380094     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logLessThanPowConcrete.proof 
380094     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 59.1ns 
380094     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
382429     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.33s 
382429     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logLessThanPowConcrete 
383188     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logLessThanPowConcrete 
383190     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 503.3ns 
383191     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logSqueeze.proof 
383191     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 48.1ns 
383192     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
385493     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.3s 
385493     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logSqueeze 
386250     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logSqueeze 
386255     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.68ms 
386261     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/booleanRules/Taclet_ifthenelse_equals.proof 
386261     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 175.2ns 
386262     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
388567     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.3s 
388567     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: ifthenelse_equals 
389326     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: ifthenelse_equals 
389329     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.36ms 
389331     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/booleanRules/Taclet_ifthenelse_equals_1.proof 
389331     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 177.3ns 
389332     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
391638     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.31s 
391638     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: ifthenelse_equals_1 
392399     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: ifthenelse_equals_1 
392401     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 737.5ns 
392402     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/booleanRules/Taclet_ifthenelse_equals_2.proof 
392402     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 48.1ns 
392403     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
394710     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.31s 
394710     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: ifthenelse_equals_2 
395485     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: ifthenelse_equals_2 
395487     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 797.6ns 
395488     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/locSet/Taclet_disjointWithSingleton1.proof 
395488     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 48.4ns 
395489     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
397811     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.32s 
397812     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: disjointWithSingleton1 
398557     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: disjointWithSingleton1 
398560     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.62ms 
398561     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/locSet/Taclet_disjointWithSingleton2.proof 
398561     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 55.1ns 
398562     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
400905     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.34s 
400905     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: disjointWithSingleton2 
401646     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: disjointWithSingleton2 
401649     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.44ms 
401650     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/locSet/Taclet_disjointArrayRanges.proof 
401650     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 53ns 
401651     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
403983     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.33s 
403983     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: disjointArrayRanges 
404747     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: disjointArrayRanges 
404757     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 7.42ms 
404758     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/locSet/Taclet_disjointArrayRangeAllFields1.proof 
404758     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 49.3ns 
404759     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
407071     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.31s 
407071     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: disjointArrayRangeAllFields1 
407838     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: disjointArrayRangeAllFields1 
407851     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 11.03ms 
407852     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/locSet/Taclet_disjointArrayRangeAllFields2.proof 
407852     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 60.7ns 
407853     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
410165     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.31s 
410165     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: disjointArrayRangeAllFields2 
410925     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: disjointArrayRangeAllFields2 
410936     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 9.42ms 
410938     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqSelfDefinition.proof 
410938     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 56.3ns 
410938     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
413250     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.31s 
413250     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqSelfDefinition 
414017     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqSelfDefinition 
414030     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 10.86ms 
414032     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqOutsideValue.proof 
414033     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 193.6ns 
414035     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
416341     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.31s 
416341     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqOutsideValue 
417106     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqOutsideValue 
417110     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.65ms 
417111     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_castedGetAny.proof 
417112     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 58ns 
417112     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
419438     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.33s 
419438     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: castedGetAny 
420183     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: castedGetAny 
420188     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.01ms 
420189     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqGetAlphaCast.proof 
420189     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 58.3ns 
420190     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
422520     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.33s 
422520     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqGetAlphaCast 
423267     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqGetAlphaCast 
423269     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 627.8ns 
423270     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqSingleton.proof 
423270     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 61.9ns 
423270     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
425594     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.32s 
425594     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqSingleton 
426360     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqSingleton 
426363     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.26ms 
426365     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqSingletonConcrete.proof 
426365     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 161.8ns 
426366     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
428668     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.3s 
428668     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqSingletonConcrete 
429433     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqSingletonConcrete 
429435     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 874.7ns 
429437     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqConcat.proof 
429437     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 57.4ns 
429438     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
431753     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.32s 
431753     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqConcat 
432518     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqConcat 
432528     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 8.27ms 
432530     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqSub.proof 
432530     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 50.8ns 
432530     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
434856     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.33s 
434856     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqSub 
435603     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqSub 
435607     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.35ms 
435608     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqReverse.proof 
435608     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 47ns 
435609     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
437940     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.33s 
437940     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqReverse 
438687     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqReverse 
438729     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 40.54ms 
438730     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqEmpty.proof 
438731     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 52.6ns 
438731     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
441052     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.32s 
441052     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqEmpty 
441822     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqEmpty 
441824     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 639.4ns 
441825     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqSingleton.proof 
441825     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 59.2ns 
441826     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
444134     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.31s 
444134     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqSingleton 
444899     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqSingleton 
444901     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 637.6ns 
444902     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqConcat.proof 
444902     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 57.4ns 
444903     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
447206     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.3s 
447206     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqConcat 
447971     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqConcat 
447974     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.08ms 
447975     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqSub.proof 
447975     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 58.3ns 
447976     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
450300     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.32s 
450300     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqSub 
451045     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqSub 
451050     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.26ms 
451051     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqReverse.proof 
451051     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 47.9ns 
451052     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
453371     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.32s 
453372     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqReverse 
454139     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqReverse 
454142     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.36ms 
454143     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_equalityToSeqGetAndSeqLenLeft.proof 
454143     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 49ns 
454143     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
456447     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.3s 
456448     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: equalityToSeqGetAndSeqLenLeft 
457215     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: equalityToSeqGetAndSeqLenLeft 
457217     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.19ms 
457218     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_equalityToSeqGetAndSeqLenRight.proof 
457219     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 55.5ns 
457219     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
459548     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.33s 
459549     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: equalityToSeqGetAndSeqLenRight 
460293     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: equalityToSeqGetAndSeqLenRight 
460298     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.67ms 
460299     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqSingletonEQ.proof 
460299     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 57.9ns 
460300     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
462638     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.34s 
462638     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqSingletonEQ 
463410     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqSingletonEQ 
463413     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.35ms 
463414     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqConcatEQ.proof 
463414     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 50.7ns 
463415     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
465739     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.32s 
465739     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqConcatEQ 
466503     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqConcatEQ 
466514     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 8.18ms 
466515     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqSubEQ.proof 
466515     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 54ns 
466515     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
468852     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.34s 
468852     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqSubEQ 
469617     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqSubEQ 
469619     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 594.2ns 
469620     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqReverseEQ.proof 
469620     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 67.5ns 
469621     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
471942     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.32s 
471942     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqReverseEQ 
472706     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqReverseEQ 
472712     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.96ms 
472714     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqEmptyEQ.proof 
472714     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 51.8ns 
472714     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
475018     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.3s 
475018     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqEmptyEQ 
475782     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqEmptyEQ 
475784     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 813.3ns 
475785     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqSingletonEQ.proof 
475785     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 52.5ns 
475786     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
478083     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.3s 
478083     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqSingletonEQ 
478847     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqSingletonEQ 
478850     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 736.1ns 
478851     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqConcatEQ.proof 
478851     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 46ns 
478851     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
481189     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.34s 
481189     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqConcatEQ 
481952     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqConcatEQ 
481956     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.1ms 
481957     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqSubEQ.proof 
481957     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 50ns 
481958     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
484269     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.31s 
484269     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqSubEQ 
485037     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqSubEQ 
485040     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.65ms 
485041     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqReverseEQ.proof 
485041     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 58.1ns 
485042     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
487373     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.33s 
487373     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqReverseEQ 
488120     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqReverseEQ 
488123     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.82ms 
488124     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqDefEQ.proof 
488124     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 57.8ns 
488125     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
490449     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.32s 
490449     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqDefEQ 
491215     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqDefEQ 
491218     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.04ms 
491220     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqDefEQ.proof 
491220     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 50ns 
491220     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
493524     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.3s 
493524     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqDefEQ 
494295     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqDefEQ 
494300     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.09ms 
494301     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqConcatWithSeqEmpty1.proof 
494301     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 57.7ns 
494302     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
496625     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.32s 
496625     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqConcatWithSeqEmpty1 
497395     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqConcatWithSeqEmpty1 
497409     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 12.46ms 
497410     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqConcatWithSeqEmpty2.proof 
497410     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 59.8ns 
497411     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
499726     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.31s 
499726     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqConcatWithSeqEmpty2 
500492     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqConcatWithSeqEmpty2 
500507     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 13.6ms 
500508     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqReverseOfSeqEmpty.proof 
500508     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 62.8ns 
500509     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
502837     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.33s 
502837     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqReverseOfSeqEmpty 
503584     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqReverseOfSeqEmpty 
503594     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 8.57ms 
503595     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_subSeqComplete.proof 
503595     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 59.3ns 
503596     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
505921     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.33s 
505921     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: subSeqComplete 
506684     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: subSeqComplete 
506695     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 9.22ms 
506696     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_subSeqTailR.proof 
506697     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 57.6ns 
506697     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
509002     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.3s 
509002     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: subSeqTailR 
509770     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: subSeqTailR 
509797     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 23.97ms 
509798     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_subSeqTailL.proof 
509798     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 51.9ns 
509799     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
512126     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.33s 
512126     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: subSeqTailL 
512888     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: subSeqTailL 
512913     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 22.6ms 
512914     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_subSeqTailEQR.proof 
512914     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 61.6ns 
512915     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
515218     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.3s 
515218     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: subSeqTailEQR 
515982     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: subSeqTailEQR 
516005     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 20.97ms 
516006     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_subSeqTailEQL.proof 
516006     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 49.9ns 
516007     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
518333     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.33s 
518333     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: subSeqTailEQL 
519098     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: subSeqTailEQL 
519112     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 12.09ms 
519113     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDef_split.proof 
519113     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 63.6ns 
519114     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
521421     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.31s 
521421     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_split 
522186     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDef_split 
522216     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 26.81ms 
522217     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDef_induction_upper.proof 
522217     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 61.9ns 
522218     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
524544     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.33s 
524544     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_induction_upper 
525307     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDef_induction_upper 
525353     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 42.33ms 
525354     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDef_induction_upper_concrete.proof 
525354     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 63.4ns 
525355     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
527662     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.31s 
527662     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_induction_upper_concrete 
528429     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDef_induction_upper_concrete 
528466     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 33.64ms 
528467     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDef_induction_lower.proof 
528467     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 59.6ns 
528468     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
530786     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.32s 
530786     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_induction_lower 
531549     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDef_induction_lower 
531590     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 37.24ms 
531591     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDef_induction_lower_concrete.proof 
531591     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 63.1ns 
531591     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
533918     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.33s 
533918     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_induction_lower_concrete 
534664     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDef_induction_lower_concrete 
534708     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 40.09ms 
534709     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDef_split_in_three.proof 
534709     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 52.5ns 
534710     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
537033     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.32s 
537033     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_split_in_three 
537798     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDef_split_in_three 
537915     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 108.97ms 
537916     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDef_empty.proof 
537916     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 61.8ns 
537917     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
540257     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.34s 
540257     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_empty 
541022     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDef_empty 
541029     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 5.66ms 
541030     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDef_one_summand.proof 
541030     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 49ns 
541031     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
543334     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.3s 
543334     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_one_summand 
544097     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDef_one_summand 
544105     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 5.78ms 
544106     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDef_lower_equals_upper.proof 
544106     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 55ns 
544107     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
546424     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.32s 
546424     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_lower_equals_upper 
547188     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDef_lower_equals_upper 
547193     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.61ms 
547194     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDefOfSeq.proof 
547194     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 58ns 
547195     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
549502     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.31s 
549502     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDefOfSeq 
550268     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDefOfSeq 
550285     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 14.25ms 
550286     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqSelfDefinitionEQ2.proof 
550287     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 60.8ns 
550287     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
552610     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.32s 
552610     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqSelfDefinitionEQ2 
553378     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqSelfDefinitionEQ2 
553388     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 8.67ms 
553389     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_indexOfSeqSingleton.proof 
553389     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 59ns 
553390     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
555711     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.32s 
555711     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: indexOfSeqSingleton 
556475     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: indexOfSeqSingleton 
556479     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.62ms 
556480     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_indexOfSeqConcatFirst.proof 
556480     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 56.1ns 
556480     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
558784     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.3s 
558784     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: indexOfSeqConcatFirst 
559548     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: indexOfSeqConcatFirst 
559564     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 14.23ms 
559565     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_indexOfSeqConcatSecond.proof 
559565     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 60.6ns 
559566     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
561894     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.33s 
561895     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: indexOfSeqConcatSecond 
562661     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: indexOfSeqConcatSecond 
562677     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 13.32ms 
562678     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_indexOfSeqSub.proof 
562678     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 57.6ns 
562679     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
565003     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.32s 
565003     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: indexOfSeqSub 
565749     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: indexOfSeqSub 
565767     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 15.63ms 
565768     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfArray2seq.proof 
565768     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 56.3ns 
565769     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
568104     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.34s 
568104     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfArray2seq 
568869     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfArray2seq 
568872     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.01ms 
568873     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getAnyOfArray2seq.proof 
568873     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 52.7ns 
568874     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
571199     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.33s 
571199     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getAnyOfArray2seq 
571964     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getAnyOfArray2seq 
571967     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.82ms 
571969     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfArray2seq.proof 
571969     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 63.3ns 
571969     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
574291     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.32s 
574292     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfArray2seq 
575038     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfArray2seq 
575044     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.34ms 
575045     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_getAnyOfNPermInv.proof 
575045     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 56.8ns 
575046     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
577371     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.33s 
577371     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getAnyOfNPermInv 
578134     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getAnyOfNPermInv 
578141     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.49ms 
578142     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqNPermRange.proof 
578142     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 47ns 
578142     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
580459     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.32s 
580460     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqNPermRange 
581226     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqNPermRange 
581296     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 63.16ms 
581297     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermTrans.proof 
581297     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 60.1ns 
581298     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
583634     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.34s 
583634     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermTrans 
584403     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermTrans 
584432     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 24.93ms 
584434     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermRefl.proof 
584434     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 177.2ns 
584435     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
586753     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.32s 
586753     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermRefl 
587518     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermRefl 
587539     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 19.17ms 
587540     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermSplit.proof 
587540     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 60.2ns 
587541     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
589860     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.32s 
589860     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermSplit 
590629     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermSplit 
590631     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 246ns 
590633     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqNPermRight.proof 
590633     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 176.4ns 
590634     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
592954     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.32s 
592954     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqNPermRight 
593718     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqNPermRight 
593912     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 182.23ms 
593914     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermFromSwap.proof 
593914     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 177.5ns 
593915     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
596248     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.33s 
596248     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermFromSwap 
597015     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermFromSwap 
597067     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 46.46ms 
597077     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermTransAlt0.proof 
597077     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 223ns 
597078     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
599409     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.33s 
599409     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermTransAlt0 
600175     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermTransAlt0 
600177     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 292.2ns 
600178     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermTransAlt1.proof 
600178     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 47.5ns 
600179     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
602482     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.3s 
602482     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermTransAlt1 
603247     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermTransAlt1 
603248     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 342.3ns 
603249     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermTransAlt2.proof 
603249     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 55.3ns 
603250     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
605571     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.32s 
605571     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermTransAlt2 
606336     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermTransAlt2 
606338     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 325.5ns 
606339     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermTransAlt3.proof 
606339     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 46.1ns 
606339     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
608661     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.32s 
608661     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermTransAlt3 
609428     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermTransAlt3 
609430     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 431.1ns 
609431     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermForall.proof 
609431     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 56.1ns 
609431     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
611755     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.32s 
611755     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermForall 
612521     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermForall 
612595     INFO  Test worker     d.u.i.k.s.SMTFocusResults Analyzing unsat core: (L_1 L_3 L_4) 
612611     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 87.25ms 
612613     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermExists.proof 
612613     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 186.3ns 
612614     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
614960     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.35s 
614960     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermExists 
615726     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermExists 
615773     INFO  Test worker     d.u.i.k.s.SMTFocusResults Analyzing unsat core: (L_1 L_3 L_5 L_6 L_7) 
615774     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 46.2ms 
615775     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm2/Taclet_schiffl_lemma_2.proof 
615775     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 49.8ns 
615785     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
618146     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.36s 
618147     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: schiffl_lemma_2 
618899     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: schiffl_lemma_2 
618900     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.8ns 
618923     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 1: 'macro split-prop' 
618985     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 2: 'rule allRight' 
619001     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 3: 'rule allRight' 
619005     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 4: 'macro split-prop' 
619010     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 5: 'rule 'seqPermDefLeft'' 
619013     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 6: 'rule 'andLeft'' 
619014     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 7: 'rule 'exLeft'' 
619015     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 8: 'macro split-prop' 
619018     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 9: 'rule  seqNPermRange' 
619020     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 10: 'instantiate var=iv with='v_x_0' occ=1' 
619022     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 11: 'rule impLeft' 
619023     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 12: 'tryclose branch' 
619176     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 13: 'rule andLeft' 
619177     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 14: 'rule andLeft' 
619178     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 15: 'instantiate var=iv with='v_y_0' occ=1' 
619179     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 16: 'rule impLeft' 
619180     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 17: 'tryclose branch' 
619291     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 18: 'rule andLeft' 
619292     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 19: 'rule andLeft' 
619293     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 20: 'rule seqNPermDefLeft' 
619295     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 21: 'instantiate var=iv with='v_x_0' occ=2' 
619296     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 22: 'rule impLeft' 
619297     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 23: 'tryclose branch' 
619462     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 24: 'rule exLeft' 
619464     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 25: 'rule andLeft' 
619465     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 26: 'rule andLeft' 
619468     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 27: 'instantiate hide var=iv with='v_y_0' occ=2' 
619469     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 28: 'rule impLeft' 
619473     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 29: 'tryclose branch' 
619587     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 30: 'rule exLeft' 
619589     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 31: 'rule andLeft' 
619590     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 32: 'rule andLeft' 
619590     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 33: 'instantiate var=iv with='jv_0' occ=1' 
619591     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 34: 'rule impLeft' 
619592     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 35: 'tryclose branch' 
619599     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 36: 'rule andLeft' 
619599     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 37: 'rule andLeft' 
619600     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 38: 'rule castAdd formula='s_0[jv_0] = v_x_0' occ=0' 
619602     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 39: 'instantiate hide var=iv with='jv_1' occ=1' 
619603     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 40: 'rule impLeft' 
619604     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 41: 'tryclose branch' 
619610     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 42: 'rule andLeft' 
619611     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 43: 'rule andLeft' 
619612     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 44: 'rule castAdd formula='s_0[jv_1] = v_y_0' occ=0' 
619613     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 45: 'instantiate var=iv  with='v_x_0'' 
619614     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 46: 'rule impLeft' 
619615     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 47: 'tryclose branch' 
619777     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 48: 'instantiate var=iv  with='v_y_0'' 
619778     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 49: 'rule impLeft' 
619779     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 50: 'tryclose branch' 
619900     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 51: 'cut 'v_x_0 = v_y_0'' 
619901     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)'' 
619904     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 53: 'rule andRight' 
619905     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 54: 'rule andRight' 
619906     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 55: 'rule andRight' 
619906     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 56: 'rule andRight' 
619907     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 57: 'rule lenOfSwap' 
619908     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 58: 'tryclose branch' 
619911     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 59: 'rule seqNPermSwapNPerm' 
619913     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 60: 'instantiate hide var='iv' with='v_x_0' occ=1' 
619914     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 61: 'instantiate hide var='jv' with='jv_0'' 
619915     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 62: 'rule impLeft' 
619916     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 63: 'tryclose branch' 
620025     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 64: 'tryclose branch' 
620029     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 65: 'rule allRight' 
620030     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 66: 'rule impRight' 
620031     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 67: 'rule andLeft' 
620032     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 68: 'instantiate var=iv with='v_iv_0'' 
620032     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 69: 'rule impLeft' 
620033     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 70: 'tryclose branch' 
620159     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 71: 'rule getOfSwap' 
620161     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 72: 'rule ifthenelse_negated' 
620162     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 73: 'rule ifthenelse_split occ=0' 
620163     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 74: 'rule andLeft' 
620163     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 75: 'rule andLeft' 
620164     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 76: 'rule andLeft' 
620165     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 77: 'rule ifthenelse_split occ=0' 
620166     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 78: 'tryclose branch' 
620284     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 79: 'rule ifthenelse_split occ=0' 
620286     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 80: 'tryclose branch' 
620395     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 81: 'tryclose branch' 
620399     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 82: 'tryclose branch' 
620404     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 83: 'rule getOfSwap' 
620405     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 84: 'rule ifthenelse_negated' 
620406     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 85: 'rule ifthenelse_split occ=0' 
620407     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 86: 'rule andLeft' 
620408     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 87: 'rule andLeft' 
620408     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 88: 'rule andLeft' 
620409     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 89: 'rule ifthenelse_split occ=0' 
620410     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 90: 'tryclose branch' 
620418     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 91: 'tryclose branch' 
620423     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 92: 'tryclose branch' 
620526     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 93: 'rule getOfSwap' 
620528     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 94: 'rule ifthenelse_negated' 
620529     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 95: 'rule ifthenelse_split occ=0' 
620530     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 96: 'rule andLeft' 
620530     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 97: 'rule andLeft' 
620531     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 98: 'rule andLeft' 
620531     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 99: 'rule ifthenelse_split occ=0' 
620532     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 100: 'tryclose branch' 
620589     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 101: 'tryclose branch' 
620595     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 102: 'tryclose branch' 
620704     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 103: 'cut '(int)s_0[v_x_0] = (int)s_0[v_y_0]'' 
620705     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 104: 'rule seqNPermInjective' 
620707     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 105: 'instantiate hide var=iv with='v_x_0'' 
620709     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 106: 'instantiate hide var=jv with='v_y_0'' 
620710     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 107: 'rule impLeft' 
620710     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 108: 'tryclose branch' 
620865     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 109: 'tryclose branch' 
620869     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 110: 'cut '(int)s_0[v_x_0] = v_x_0'' 
620870     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)'' 
620871     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 112: 'rule andRight' 
620872     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 113: 'rule andRight' 
620873     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 114: 'rule andRight' 
620874     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 115: 'rule andRight' 
620874     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 116: 'tryclose branch' 
620883     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 117: 'rule seqNPermSwapNPerm' 
620884     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 118: 'instantiate hide var=iv with='v_y_0'' 
620890     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 119: 'instantiate hide var=jv with='jv_1'' 
620891     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 120: 'tryclose branch' 
620990     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 121: 'rule allRight' 
620992     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 122: 'rule impRight' 
620993     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 123: 'rule andLeft' 
620993     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 124: 'instantiate var=iv with='v_iv_0'' 
620994     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 125: 'rule impLeft' 
620995     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 126: 'tryclose branch' 
621100     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 127: 'rule getOfSwap' 
621101     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 128: 'rule ifthenelse_negated' 
621102     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 129: 'rule ifthenelse_split occ=0' 
621103     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 130: 'rule andLeft' 
621104     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 131: 'rule andLeft' 
621105     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 132: 'rule andLeft' 
621105     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 133: 'rule ifthenelse_split occ=0' 
621106     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 134: 'tryclose branch' 
621189     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 135: 'rule ifthenelse_split occ=0' 
621191     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 136: 'tryclose branch' 
621265     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 137: 'instantiate var=iv with='v_y_0'' 
621265     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 138: 'rule impLeft' 
621266     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 139: 'tryclose branch' 
621270     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 140: 'tryclose branch' 
621275     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 141: 'tryclose branch' 
621279     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 142: 'tryclose branch' 
621397     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 143: 'rule getOfSwap' 
621399     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 144: 'rule ifthenelse_negated' 
621399     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 145: 'rule ifthenelse_split occ=0' 
621401     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 146: 'tryclose branch' 
621410     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 147: 'tryclose branch' 
621499     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 148: 'tryclose branch' 
625045     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 149: 'cut  '(int)s_0[v_y_0] = v_y_0'' 
625046     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)'' 
625052     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 151: 'rule andRight' 
625053     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 152: 'rule andRight' 
625054     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 153: 'rule andRight' 
625056     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 154: 'rule andRight' 
625057     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 155: 'tryclose branch' 
625065     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 156: 'rule seqNPermSwapNPerm' 
625067     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 157: 'instantiate hide var=iv with='v_x_0'' 
625068     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 158: 'instantiate hide var=jv with='jv_0'' 
625068     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 159: 'rule impLeft' 
625069     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 160: 'tryclose branch' 
625161     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 161: 'tryclose branch' 
625164     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 162: 'rule allRight' 
625170     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 163: 'rule impRight' 
625171     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 164: 'rule andLeft' 
625172     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 165: 'instantiate var=iv with='v_iv_0'' 
625172     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 166: 'rule impLeft' 
625173     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 167: 'tryclose branch' 
625267     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 168: 'rule getOfSwap' 
625269     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 169: 'rule ifthenelse_negated' 
625270     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 170: 'rule ifthenelse_split occ=0' 
625271     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 171: 'rule andLeft' 
625271     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 172: 'rule andLeft' 
625272     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 173: 'rule andLeft' 
625273     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 174: 'rule ifthenelse_split occ=0' 
625274     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 175: 'tryclose branch' 
625347     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 176: 'rule ifthenelse_split occ=0' 
625348     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 177: 'tryclose branch' 
625422     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 178: 'tryclose branch' 
625426     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 179: 'tryclose branch' 
625430     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 180: 'rule getOfSwap' 
625431     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 181: 'rule ifthenelse_negated' 
625432     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 182: 'rule ifthenelse_split occ=0' 
625432     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 183: 'tryclose branch' 
625442     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 184: 'tryclose branch' 
625519     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 185: 'rule getOfSwap' 
625520     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 186: 'rule ifthenelse_negated' 
625521     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 187: 'rule ifthenelse_split occ=0' 
625522     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 188: 'tryclose branch' 
625593     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 189: 'tryclose branch' 
625601     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 190: 'cut '(int)s_0[v_x_0]=v_y_0'' 
625602     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)'' 
625606     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 192: 'rule andRight' 
625607     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 193: 'rule andRight' 
625607     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 194: 'rule andRight' 
625608     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 195: 'rule andRight' 
625608     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 196: 'tryclose branch' 
625618     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 197: 'rule seqNPermSwapNPerm' 
625620     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 198: 'instantiate hide var=iv with='jv_0'' 
625621     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 199: 'instantiate hide var=jv with='v_x_0'' 
625621     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 200: 'rule impLeft' 
625622     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 201: 'tryclose branch' 
625709     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 202: 'rule seqNPermSwapNPerm formula='seqNPerm(seqSwap(s_0, jv_0, v_x_0))'' 
625710     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 203: 'instantiate hide var=iv with='jv_0'' 
625711     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 204: 'instantiate hide var=jv with='v_y_0'' 
625712     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 205: 'rule impLeft' 
625712     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 206: 'tryclose branch' 
625801     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 207: 'tryclose branch' 
625805     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 208: 'rule allRight' 
625806     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 209: 'rule impRight' 
625806     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 210: 'rule andLeft' 
625807     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 211: 'instantiate var=iv with='v_iv_0'' 
625807     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 212: 'rule impLeft' 
625808     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 213: 'tryclose branch' 
625903     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 214: 'rule getOfSwap' 
625904     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 215: 'rule ifthenelse_negated' 
625905     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 216: 'rule ifthenelse_split occ=0' 
625906     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 217: 'rule andLeft' 
625906     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 218: 'rule andLeft' 
625907     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 219: 'rule andLeft' 
625907     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 220: 'rule ifthenelse_split occ=0' 
625908     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 221: 'rule getOfSwap' 
625909     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 222: 'rule ifthenelse_negated' 
625909     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 223: 'rule ifthenelse_split occ=0' 
625911     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 224: 'rule andLeft' 
625912     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 225: 'rule andLeft' 
625913     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 226: 'rule andLeft' 
625913     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 227: 'rule ifthenelse_split occ=0' 
625914     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 228: 'tryclose branch' 
626002     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 229: 'rule ifthenelse_split occ=0' 
626003     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 230: 'tryclose branch' 
626009     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 231: 'tryclose branch' 
626086     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 232: 'tryclose branch' 
626165     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 233: 'rule ifthenelse_split' 
626166     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 234: 'rule getOfSwap' 
626167     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 235: 'rule ifthenelse_negated' 
626168     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 236: 'rule ifthenelse_split occ=0' 
626169     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 237: 'rule andLeft' 
626170     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 238: 'rule andLeft' 
626170     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 239: 'rule andLeft' 
626171     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 240: 'rule ifthenelse_split occ=0' 
626172     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 241: 'tryclose branch' 
626323     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 242: 'tryclose branch' 
626329     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 243: 'tryclose branch' 
626416     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 244: 'rule getOfSwap' 
626417     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 245: 'rule ifthenelse_negated' 
626418     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 246: 'rule ifthenelse_split occ=0' 
626419     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 247: 'rule andLeft' 
626420     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 248: 'rule andLeft' 
626420     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 249: 'rule andLeft' 
626421     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 250: 'rule ifthenelse_split occ=0' 
626422     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 251: 'tryclose branch' 
626427     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 252: 'rule ifthenelse_split occ=0' 
626428     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 253: 'tryclose branch' 
626506     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 254: 'tryclose branch' 
626511     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 255: 'tryclose branch' 
626517     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 256: 'tryclose branch' 
626613     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 257: 'rule getOfSwap' 
626614     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 258: 'rule ifthenelse_negated' 
626615     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 259: 'rule ifthenelse_split occ=0' 
626615     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 260: 'rule andLeft' 
626616     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 261: 'rule andLeft' 
626616     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 262: 'rule andLeft' 
626617     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 263: 'rule ifthenelse_split occ=0' 
626617     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 264: 'tryclose branch' 
626669     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 265: 'rule ifthenelse_split occ=0' 
626670     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 266: 'rule getOfSwap' 
626671     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 267: 'rule ifthenelse_negated' 
626671     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 268: 'rule ifthenelse_split occ=0' 
626672     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 269: 'tryclose branch' 
626677     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 270: 'tryclose branch' 
626682     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 271: 'tryclose branch' 
626793     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 272: 'tryclose branch' 
626876     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 273: 'rule getOfSwap' 
626877     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 274: 'rule ifthenelse_negated' 
626878     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 275: 'rule ifthenelse_split occ=0' 
626879     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 276: 'tryclose branch' 
627038     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 277: 'tryclose branch' 
627122     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 278: 'cut 'int::seqGet(s_0, v_y_0)=v_x_0'' 
627122     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 279: 'tryclose branch' 
630121     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 280: 'rule seqNPermSwapNPerm' 
630126     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 281: 'instantiate hide var=iv with='jv_1'' 
630128     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 282: 'instantiate hide var=jv with='v_y_0'' 
630128     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 283: 'rule impLeft' 
630129     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 284: 'tryclose branch' 
630240     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 285: 'rule seqNPermSwapNPerm formula='seqNPerm(seqSwap(s_0,jv_1,v_y_0))'' 
630241     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 286: 'instantiate hide var=iv with='jv_1'' 
630243     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 287: 'instantiate hide var=jv with='v_x_0'' 
630243     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 288: 'rule impLeft' 
630244     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 289: 'tryclose branch' 
630345     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 290: 'tryclose branch' 
633293     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 291: 'tryclose branch' 
636400     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 292: 'rule seqNPermSwapNPerm formula='seqNPerm(s_0)'' 
636405     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 293: 'instantiate hide var=iv with='v_x_0'' 
636406     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 294: 'instantiate hide var=jv with='jv_0'' 
636407     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 295: 'rule impLeft' 
636407     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 296: 'tryclose branch' 
636516     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 297: 'rule seqNPermSwapNPerm formula='seqNPerm(seqSwap(s_0,v_x_0,jv_0))'' 
636518     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 298: 'instantiate hide var=iv with='v_y_0'' 
636519     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 299: 'instantiate hide var=jv with='jv_1'' 
636520     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)' ...' 
636522     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 301: 'tryclose branch' 
637673     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm2/Taclet_schiffl_thm_1.proof 
637673     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 80ns 
637674     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
640083     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.41s 
640083     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: schiffl_thm_1 
640873     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: schiffl_thm_1 
640874     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 5.7ns 
640875     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 1: 'macro split-prop' 
640880     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 2: 'rule schiffl_lemma_2 formula='seqPerm(f_s, f_t)'' 
640891     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 3: 'instantiate hide var=x with='f_x'' 
640894     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 4: 'instantiate hide var=y with='f_y'' 
640895     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 5: 'rule impLeft' 
640896     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 6: 'tryclose branch' 
640900     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 7: 'rule exLeft' 
640901     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 8: 'macro split-prop' 
640903     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 9: 'rule seqPermDef occ=1' 
640906     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 10: 'rule andRight' 
640907     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 11: 'tryclose branch' 
640914     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 12: 'instantiate hide var=s with='r_0'' 
640916     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 13: 'rule andRight' 
640916     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 14: 'tryclose branch' 
640959     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 15: 'rule allRight' 
640960     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 16: 'rule impRight' 
640961     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 17: 'instantiate hide var=iv with='iv_0'' 
640961     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 18: 'rule impLeft' 
640962     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 19: 'tryclose branch' 
641026     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 20: 'rule andLeft' 
641027     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 21: 'rule seqNPermRange' 
641028     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 22: 'instantiate hide var=iv with='iv_0'' 
641029     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 23: 'rule impLeft' 
641029     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 24: 'tryclose branch' 
641032     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 25: 'rule andLeft' 
641033     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 26: 'rule andLeft' 
641033     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 27: 'rule seqNPermRange' 
641034     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 28: 'instantiate hide var=iv with='f_x'' 
641035     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 29: 'rule impLeft' 
641035     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 30: 'tryclose branch' 
641117     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 31: 'rule andLeft' 
641118     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 32: 'rule andLeft' 
641119     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 33: 'rule seqNPermRange' 
641120     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 34: 'instantiate hide var=iv with='f_y'' 
641120     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 35: 'rule impLeft' 
641121     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 36: 'tryclose branch' 
641211     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 37: 'rule andLeft' 
641212     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 38: 'rule andLeft' 
641212     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 39: 'rule getOfSeqDef occ=0' 
641213     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 40: 'rule getOfSeqDef' 
641213     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 41: 'rule ifthenelse_split occ=0' 
641214     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 42: 'rule andLeft occ=0' 
641215     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 43: 'rule sub_zero_2 occ=0' 
641215     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 44: 'rule ifthenelse_split occ=2' 
641216     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 45: 'rule andLeft' 
641216     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 46: 'rule sub_zero_2 occ=0' 
641216     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 47: 'rule add_zero_right occ=0' 
641217     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 48: 'rule add_zero_right occ=0' 
641217     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 49: 'rule add_zero_right occ=0' 
641217     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 50: 'rule add_zero_right occ=0' 
641218     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 51: 'rule add_zero_right occ=0' 
641218     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 52: 'rule add_zero_right occ=0' 
641218     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 53: 'rule ifthenelse_split occ=0' 
641219     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 54: 'rule ifthenelse_split occ=0' 
641220     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 55: 'tryclose branch' 
641222     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 56: 'tryclose branch' 
641260     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 57: 'rule ifthenelse_split occ=0' 
641261     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 58: 'tryclose branch' 
641315     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 59: 'rule ifthenelse_split occ=0' 
641316     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 60: 'rule seqNPermInjective' 
641317     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 61: 'instantiate hide var=iv with='iv_0'' 
641318     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 62: 'instantiate hide var=jv with='f_y'' 
641319     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 63: 'rule impLeft' 
641319     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 64: 'tryclose branch' 
641365     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 65: 'tryclose branch' 
641367     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 66: 'rule ifthenelse_split occ=0' 
641368     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 67: 'rule seqNPermInjective' 
641370     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 68: 'instantiate hide var=iv with='iv_0'' 
641371     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 69: 'instantiate hide var=jv with='f_x'' 
641371     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 70: 'rule impLeft' 
641372     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 71: 'tryclose branch' 
641416     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 72: 'tryclose branch' 
641418     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 73: 'tryclose branch' 
641421     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 74: 'tryclose branch' 
641468     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 75: 'tryclose branch' 
641517     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_eqSameSeq.proof 
641517     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 73.8ns 
641518     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
643857     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.34s 
643857     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: eqSameSeq 
644649     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: eqSameSeq 
644691     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 37.37ms