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

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

tests
0

failures
0

ignored
10m32.19s

duration
100%

successful

Tests

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

Standard output

304        INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src/test/resources/testcase/dummyTrue.key 
326        DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 9.66ms 
524        INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
555        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)

1463       DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for Meta 
1465       DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for Meta 
1470       DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for Meta 
1470       DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for Meta 
3429       DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for JavaBigintExpression 
8725       DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 8.2s 
8784       INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof dummyTrue.key 
8817       DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 82.6ns 
8831       INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/firstOrder/Taclet_eqTermCut.proof 
8832       DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 1.74ms 
8837       INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
11617      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.78s 
11619      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: eqTermCut 
12490      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: eqTermCut 
12513      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 17.81ms 
12522      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/firstOrder/Taclet_equivAllRight.proof 
12522      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 162.7ns 
12523      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
15132      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.61s 
15133      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: equivAllRight 
16009      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: equivAllRight 
16037      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 20.68ms 
16042      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_irrflConcrete1.proof 
16042      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 430.61ns 
16046      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
18564      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.52s 
18565      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: irrflConcrete1 
19386      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: irrflConcrete1 
19393      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.07ms 
19396      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_irrflConcrete2.proof 
19396      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 371.01ns 
19398      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
21822      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.42s 
21823      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: irrflConcrete2 
22604      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: irrflConcrete2 
22610      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.85ms 
22612      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_cancel_gtPos.proof 
22613      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 541.51ns 
22614      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
25025      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.41s 
25026      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: cancel_gtPos 
25832      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: cancel_gtPos 
25875      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 40.2ms 
25877      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_cancel_gtNeg.proof 
25877      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 170.2ns 
25880      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
28272      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.39s 
28272      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: cancel_gtNeg 
29051      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: cancel_gtNeg 
29071      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 17.23ms 
29075      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intRulesIgnoringOF/Taclet_moduloIntIsInInt.proof 
29075      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 410.41ns 
29076      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
31467      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.39s 
31468      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: moduloIntIsInInt 
32289      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: moduloIntIsInInt 
32292      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 828.21ns 
32295      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intRulesIgnoringOF/Taclet_moduloLongIsInLong.proof 
32296      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 353.61ns 
32297      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
34672      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.37s 
34672      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: moduloLongIsInLong 
35444      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: moduloLongIsInLong 
35447      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 628.01ns 
35450      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intRulesIgnoringOF/Taclet_moduloShortIsInShort.proof 
35450      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 220.7ns 
35451      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
37820      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.37s 
37821      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: moduloShortIsInShort 
38590      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: moduloShortIsInShort 
38593      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 628.51ns 
38595      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intRulesIgnoringOF/Taclet_moduloByteIsInByte.proof 
38595      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 315ns 
38596      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
40939      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.34s 
40939      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: moduloByteIsInByte 
41705      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: moduloByteIsInByte 
41708      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 629.91ns 
41709      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intRulesIgnoringOF/Taclet_moduloCharIsInChar.proof 
41710      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 106.4ns 
41710      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
44059      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.35s 
44059      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: moduloCharIsInChar 
44860      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: moduloCharIsInChar 
44866      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.66ms 
44869      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_div_unique1.proof 
44869      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 134.1ns 
44870      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
47190      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.32s 
47190      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: div_unique1 
47956      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: div_unique1 
48044      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 80.7ms 
48046      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_div_unique2.proof 
48046      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 159.5ns 
48047      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
50354      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.31s 
50354      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: div_unique2 
51114      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: div_unique2 
51169      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 52.25ms 
51174      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_div_exists.proof 
51174      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 393.11ns 
51176      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
53507      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.33s 
53507      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: div_exists 
54267      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: div_exists 
54423      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 147.78ms 
54427      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_div_one.proof 
54427      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 370.5ns 
54428      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
56761      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.33s 
56762      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: div_one 
57499      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: div_one 
57504      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.84ms 
57506      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdiv_one.proof 
57506      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 208.6ns 
57507      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
59834      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.33s 
59835      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdiv_one 
60571      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdiv_one 
60574      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.29ms 
60578      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_div_zero.proof 
60578      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 313.8ns 
60580      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
62899      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.32s 
62900      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: div_zero 
63719      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: div_zero 
63779      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 55.93ms 
63782      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divResZero1.proof 
63783      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 152ns 
63784      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
66117      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.33s 
66117      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divResZero1 
66885      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divResZero1 
66900      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 11.95ms 
66902      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divResZero2.proof 
66902      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 108.4ns 
66903      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
69218      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.31s 
69218      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divResZero2 
69975      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divResZero2 
69989      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 11.57ms 
69991      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divResOne1.proof 
69991      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 129.5ns 
69992      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
72303      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.31s 
72304      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divResOne1 
73065      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divResOne1 
73080      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 12.33ms 
73081      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divResOne2.proof 
73081      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 115.1ns 
73082      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
75410      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.33s 
75411      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divResOne2 
76174      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divResOne2 
76189      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 11.67ms 
76195      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_div_cancel1.proof 
76197      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 1.69ms 
76198      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
78562      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.36s 
78562      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: div_cancel1 
79322      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: div_cancel1 
79345      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 19.95ms 
79347      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_div_cancel2.proof 
79347      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 112.6ns 
79348      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
81656      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.31s 
81656      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: div_cancel2 
82411      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: div_cancel2 
82414      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.09ms 
82415      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divAddMultDenom.proof 
82415      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 84.4ns 
82416      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
84716      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.3s 
84716      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divAddMultDenom 
85472      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divAddMultDenom 
85511      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 33.39ms 
85512      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divMinus.proof 
85512      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 136.8ns 
85513      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
87806      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.29s 
87806      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divMinus 
88562      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divMinus 
88615      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 47.5ms 
88618      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divMinusDenom.proof 
88618      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 300.3ns 
88619      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
90937      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.32s 
90937      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divMinusDenom 
91669      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divMinusDenom 
91709      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 35.06ms 
91711      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divLeastDPos.proof 
91711      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 117.1ns 
91712      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
94029      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.32s 
94030      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divLeastDPos 
94769      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divLeastDPos 
94777      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 5.09ms 
94780      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divLeastDNeg.proof 
94781      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 1.02ms 
94782      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
97093      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.31s 
97094      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divLeastDNeg 
97824      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divLeastDNeg 
97838      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 10.39ms 
97840      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divGreatestDPos.proof 
97840      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 326.31ns 
97843      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
100158     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.32s 
100159     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divGreatestDPos 
100914     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divGreatestDPos 
100925     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 8.86ms 
100928     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divGreatestDNeg.proof 
100928     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 309.9ns 
100929     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
103234     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.31s 
103235     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divGreatestDNeg 
103998     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divGreatestDNeg 
104006     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 5.54ms 
104007     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divIncreasingPos.proof 
104007     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 123.7ns 
104008     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
106303     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.3s 
106304     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divIncreasingPos 
107057     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divIncreasingPos 
107064     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 5.38ms 
107066     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divIncreasingNeg.proof 
107066     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 180.2ns 
107067     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
109386     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.32s 
109386     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divIncreasingNeg 
110139     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divIncreasingNeg 
110146     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.98ms 
110147     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdiv_zero.proof 
110147     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 124.9ns 
110148     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
112443     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.29s 
112444     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdiv_zero 
113209     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdiv_zero 
113212     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.44ms 
113214     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdivPulloutMinusNum.proof 
113214     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 98.1ns 
113214     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
115508     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.29s 
115509     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdivPulloutMinusNum 
116265     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdivPulloutMinusNum 
116274     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 7.63ms 
116276     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdivPulloutMinusDenom.proof 
116276     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 119.1ns 
116277     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
118587     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.31s 
118587     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdivPulloutMinusDenom 
119339     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdivPulloutMinusDenom 
119392     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 47.83ms 
119395     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdiv_uniquePosPos.proof 
119395     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 322.5ns 
119396     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
121704     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.31s 
121704     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdiv_uniquePosPos 
122479     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdiv_uniquePosPos 
122508     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 20.17ms 
122510     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdiv_uniquePosNeg.proof 
122511     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 316.61ns 
122512     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
124903     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.39s 
124903     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdiv_uniquePosNeg 
125636     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdiv_uniquePosNeg 
125655     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 15.51ms 
125656     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdiv_uniqueNegPos.proof 
125656     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 113.3ns 
125657     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
128008     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.35s 
128009     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdiv_uniqueNegPos 
128746     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdiv_uniqueNegPos 
128764     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 15.23ms 
128766     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdiv_uniqueNegNeg.proof 
128766     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 130.2ns 
128767     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
131102     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.34s 
131103     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdiv_uniqueNegNeg 
131840     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdiv_uniqueNegNeg 
131857     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 14.22ms 
131859     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdivMultDenom1.proof 
131859     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 116.9ns 
131860     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
134192     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.33s 
134192     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdivMultDenom1 
134952     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdivMultDenom1 
134992     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 34.65ms 
134998     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdivMultDenom2.proof 
134998     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 126.1ns 
134999     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
137311     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.31s 
137311     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdivMultDenom2 
138066     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdivMultDenom2 
138068     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 929.71ns 
138069     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_mod_geZero.proof 
138070     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 89.5ns 
138070     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
140369     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.3s 
140369     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: mod_geZero 
141123     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: mod_geZero 
141128     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.37ms 
141130     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_mod_lessDenom.proof 
141130     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 318ns 
141131     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
143458     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.33s 
143458     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: mod_lessDenom 
144216     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: mod_lessDenom 
144224     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 5.48ms 
144225     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmod_NumPos.proof 
144225     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 95.3ns 
144226     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
146537     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.31s 
146537     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmod_NumPos 
147292     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmod_NumPos 
147312     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 17.78ms 
147314     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmod_NumNeg.proof 
147315     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 653.61ns 
147315     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
149650     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.33s 
149651     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmod_NumNeg 
150419     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmod_NumNeg 
150438     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 15.87ms 
150440     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmod_geZero.proof 
150441     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 323.2ns 
150442     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
152774     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.33s 
152775     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmod_geZero 
153542     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmod_geZero 
153550     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 5.87ms 
153552     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmodNumZero.proof 
153553     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 272.3ns 
153554     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
155889     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.33s 
155889     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmodNumZero 
156662     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmodNumZero 
156665     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.35ms 
156668     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmod_pulloutminusNum.proof 
156668     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 320.4ns 
156669     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
159051     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.38s 
159051     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmod_pulloutminusNum 
159791     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmod_pulloutminusNum 
159796     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.44ms 
159797     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmod_pulloutminusDenom.proof 
159797     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 93.2ns 
159798     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
162159     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.36s 
162159     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmod_pulloutminusDenom 
162893     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmod_pulloutminusDenom 
162897     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.44ms 
162899     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmodUnique1.proof 
162899     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 105.3ns 
162900     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
165268     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.37s 
165269     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmodUnique1 
166008     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmodUnique1 
166084     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 67.21ms 
166086     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmodUnique2.proof 
166086     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 207.1ns 
166087     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
168403     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.32s 
168403     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmodUnique2 
169162     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmodUnique2 
169238     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 66.82ms 
169240     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_intDivRem.proof 
169241     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 181.5ns 
169241     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
171527     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.29s 
171527     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: intDivRem 
172278     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: intDivRem 
172281     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.46ms 
172282     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmodjmod.proof 
172282     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 89.7ns 
172283     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
174562     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.28s 
174562     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmodjmod 
175310     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmodjmod 
175347     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 31.77ms 
175349     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmodDivisible.proof 
175349     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 227.7ns 
175350     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
177639     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.29s 
177639     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmodDivisible 
178388     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmodDivisible 
178416     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 24.54ms 
178417     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmodDivisibleRep.proof 
178418     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 101.3ns 
178418     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
180694     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.28s 
180694     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmodDivisibleRep 
181444     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmodDivisibleRep 
181447     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.06ms 
181448     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdivAddMultDenom.proof 
181448     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 69.2ns 
181449     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
183729     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.28s 
183729     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdivAddMultDenom 
184495     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdivAddMultDenom 
184634     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 128ms 
184636     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmodAltZero.proof 
184636     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 95.7ns 
184637     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
186922     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.29s 
186922     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmodAltZero 
187692     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmodAltZero 
187703     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 8.48ms 
187705     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmodAddMultDenomZero.proof 
187706     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 247.7ns 
187707     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
190019     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.31s 
190020     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmodAddMultDenomZero 
190746     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmodAddMultDenomZero 
190761     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 12.73ms 
190764     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_polyDiv_zero.proof 
190764     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 100.4ns 
190765     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
193073     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.31s 
193074     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: polyDiv_zero 
193801     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: polyDiv_zero 
193817     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 13.58ms 
193818     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_polyMod_ltdivDenom.proof 
193818     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 82.4ns 
193819     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
196120     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.3s 
196120     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: polyMod_ltdivDenom 
196844     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: polyMod_ltdivDenom 
196856     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 6.39ms 
196858     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_empty.proof 
196858     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 74.4ns 
196859     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
199148     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.29s 
199149     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_empty 
199895     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_empty 
199899     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.57ms 
199902     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_induction_upper.proof 
199902     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 248.9ns 
199903     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
202185     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.28s 
202185     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_upper 
202935     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_induction_upper 
202939     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.84ms 
202941     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_induction_lower.proof 
202941     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 86ns 
202942     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
205229     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.29s 
205229     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_lower 
205978     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_induction_lower 
206001     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 20.04ms 
206003     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_bounds.proof 
206003     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 73.6ns 
206003     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
208311     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.31s 
208311     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_bounds 
209068     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_bounds 
209084     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 13.74ms 
209090     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_bounds2.proof 
209090     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 324.4ns 
209091     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
211400     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.31s 
211400     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_bounds2 
212153     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_bounds2 
212168     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 12.76ms 
212169     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_induction_upper2.proof 
212169     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 85.1ns 
212170     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
214454     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.28s 
214454     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_upper2 
215208     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_induction_upper2 
215212     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.66ms 
215213     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_induction_upper_concrete.proof 
215213     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 90ns 
215214     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
217494     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.28s 
217494     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_upper_concrete 
218248     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_induction_upper_concrete 
218253     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.75ms 
218254     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_induction_upper_concrete_2.proof 
218254     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 96.2ns 
218255     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
220547     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.29s 
220547     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_upper_concrete_2 
221298     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_induction_upper_concrete_2 
221303     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.75ms 
221305     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_induction_upper2_concrete.proof 
221305     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 65.3ns 
221305     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
223591     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.29s 
223591     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_upper2_concrete 
224345     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_induction_upper2_concrete 
224348     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.44ms 
224349     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_induction_lower_concrete.proof 
224349     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 85.9ns 
224350     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
226659     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.31s 
226659     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_lower_concrete 
227386     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_induction_lower_concrete 
227388     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 692.51ns 
227389     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_induction_lower2.proof 
227389     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 64.8ns 
227390     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
229695     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.31s 
229695     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_lower2 
230422     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_induction_lower2 
230426     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.22ms 
230427     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_induction_lower2_concrete.proof 
230428     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 98.4ns 
230428     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
232731     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.3s 
232731     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_lower2_concrete 
233457     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_induction_lower2_concrete 
233459     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.08ms 
233461     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_positive.proof 
233461     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 57.4ns 
233461     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
235768     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.31s 
235769     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_positive 
236520     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_positive 
236566     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 43.85ms 
236569     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_upper_bound.proof 
236569     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 243.4ns 
236570     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
238860     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.29s 
238860     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_upper_bound 
239609     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_upper_bound 
239653     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 40.72ms 
239656     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_lower_bound.proof 
239656     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 231.1ns 
239657     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
241951     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.29s 
241951     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_lower_bound 
242705     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_lower_bound 
242745     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 36.73ms 
242747     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_positive_lower_bound_element.proof 
242747     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 248.1ns 
242748     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
245051     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.3s 
245051     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_positive_lower_bound_element 
245800     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_positive_lower_bound_element 
245851     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 47.32ms 
245853     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_sub_same_index.proof 
245853     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 79.5ns 
245854     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
248134     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.28s 
248134     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_sub_same_index 
248884     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_sub_same_index 
248919     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 30.87ms 
248920     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_less_same_index.proof 
248920     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 83.4ns 
248921     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
251201     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.28s 
251201     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_less_same_index 
251953     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_less_same_index 
252010     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 52.7ms 
252012     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_equal_except_one_index.proof 
252012     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 73.9ns 
252013     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
254319     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.31s 
254319     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_equal_except_one_index 
255069     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_equal_except_one_index 
255096     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 24.02ms 
255097     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_is_max.proof 
255098     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 87.9ns 
255098     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
257398     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.3s 
257398     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_is_max 
258122     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_is_max 
258141     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 16.03ms 
258142     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_is_max2.proof 
258142     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 73.3ns 
258143     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
260437     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.29s 
260437     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_is_max2 
261162     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_is_max2 
261186     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 21.27ms 
261187     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_is_max3.proof 
261188     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 91.4ns 
261188     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
263483     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.29s 
263483     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_is_max3 
264209     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_is_max3 
264229     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 17.3ms 
264231     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_is_max4.proof 
264231     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 80.6ns 
264232     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
266539     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.31s 
266539     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_is_max4 
267288     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_is_max4 
267315     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 24.68ms 
267317     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_lt_max.proof 
267317     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 74.1ns 
267318     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
269601     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.28s 
269601     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_lt_max 
270351     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_lt_max 
270375     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 21.68ms 
270377     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_lt_max2.proof 
270377     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 89.2ns 
270378     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
272665     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.29s 
272666     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_lt_max2 
273418     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_lt_max2 
273445     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 23.46ms 
273447     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_lt_max3.proof 
273448     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 226.3ns 
273450     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
275742     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.29s 
275742     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_lt_max3 
276494     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_lt_max3 
276518     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 21.08ms 
276519     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_lt_max4.proof 
276519     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 82.5ns 
276520     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
278812     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.29s 
278812     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_lt_max4 
279561     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_lt_max4 
279582     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 17.8ms 
279583     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_gt0.proof 
279583     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 82.8ns 
279584     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
281857     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.27s 
281857     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_gt0 
282611     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_gt0 
282637     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 23ms 
282639     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_gt0_alt.proof 
282640     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 269.2ns 
282641     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
284979     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.34s 
284980     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_gt0_alt 
285736     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_gt0_alt 
285759     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 21.15ms 
285761     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_add_concrete.proof 
285761     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 92.9ns 
285761     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
288079     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.32s 
288079     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_add_concrete 
288806     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_add_concrete 
288814     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 5.6ms 
288815     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bprod/Taclet_bprod_all_positive.proof 
288815     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 65.8ns 
288816     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
291153     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.34s 
291155     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bprod_all_positive 
291883     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bprod_all_positive 
291900     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 14.53ms 
291902     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bprod/Taclet_bprod_split.proof 
291902     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 63.4ns 
291902     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
294210     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.31s 
294210     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bprod_split 
294939     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bprod_split 
294943     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.96ms 
294944     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powConcrete0.proof 
294945     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 68.4ns 
294945     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
297300     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.35s 
297300     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powConcrete0 
298037     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powConcrete0 
298040     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 633.31ns 
298041     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powConcrete1.proof 
298041     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 83.8ns 
298042     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
300334     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.29s 
300334     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powConcrete1 
301081     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powConcrete1 
301083     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 749.41ns 
301085     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powSplitFactor.proof 
301085     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 54.3ns 
301085     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
303362     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.28s 
303362     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powSplitFactor 
304110     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powSplitFactor 
304118     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.58ms 
304119     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powAdd.proof 
304119     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 89.1ns 
304120     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
306411     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.29s 
306412     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powAdd 
307173     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powAdd 
307180     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.32ms 
307182     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powMono.proof 
307182     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 151.6ns 
307183     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
309511     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.33s 
309511     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powMono 
310272     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powMono 
310286     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 11.53ms 
310288     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powMonoConcrete.proof 
310288     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 229.5ns 
310289     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
312625     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.34s 
312626     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powMonoConcrete 
313395     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powMonoConcrete 
313399     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.29ms 
313400     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powMonoConcreteRight.proof 
313400     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 69.9ns 
313401     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
315754     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.35s 
315754     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powMonoConcreteRight 
316520     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powMonoConcreteRight 
316523     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 624.01ns 
316524     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powPositive.proof 
316524     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 74ns 
316525     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
318852     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.33s 
318852     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powPositive 
319617     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powPositive 
319625     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.7ms 
319627     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powPositiveConcrete.proof 
319632     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 276.8ns 
319633     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
321966     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.33s 
321966     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powPositiveConcrete 
322728     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powPositiveConcrete 
322730     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 604.51ns 
322732     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powGeq1Concrete.proof 
322732     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 80.1ns 
322732     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
325086     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.35s 
325086     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powGeq1Concrete 
325828     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powGeq1Concrete 
325830     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 594.01ns 
325831     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_pow2InIntLower.proof 
325831     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 76.7ns 
325832     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
328191     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.36s 
328191     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: pow2InIntLower 
328932     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: pow2InIntLower 
328935     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 614.81ns 
328937     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_pow2InIntUpper.proof 
328937     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 224.3ns 
328938     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
331298     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.36s 
331299     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: pow2InIntUpper 
332037     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: pow2InIntUpper 
332042     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.12ms 
332044     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logSelfConcrete.proof 
332044     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 90.9ns 
332045     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
334421     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.38s 
334421     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logSelfConcrete 
335176     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logSelfConcrete 
335184     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 6.47ms 
335186     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_log1Concrete.proof 
335186     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 85.1ns 
335186     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
337464     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.28s 
337465     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: log1Concrete 
338215     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: log1Concrete 
338220     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.45ms 
338222     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logProduct.proof 
338223     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 235.2ns 
338228     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
340547     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.32s 
340547     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logProduct 
341310     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logProduct 
341318     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 5.11ms 
341319     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logTimesBaseConcrete.proof 
341319     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 70.8ns 
341320     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
343665     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.35s 
343666     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logTimesBaseConcrete 
344424     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logTimesBaseConcrete 
344429     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.27ms 
344430     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logProdIdentity.proof 
344430     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 70.2ns 
344431     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
346795     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.36s 
346795     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logProdIdentity 
347551     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logProdIdentity 
347566     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 12.89ms 
347568     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logProdIdentityConcrete.proof 
347568     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 93.6ns 
347568     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
349902     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.33s 
349902     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logProdIdentityConcrete 
350657     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logProdIdentityConcrete 
350660     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.82ms 
350662     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logPowIdentity.proof 
350662     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 61.1ns 
350663     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
352967     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.3s 
352967     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logPowIdentity 
353733     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logPowIdentity 
353736     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.3ms 
353737     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logPowIdentityConcrete.proof 
353737     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 87.4ns 
353738     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
356070     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.33s 
356070     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logPowIdentityConcrete 
356828     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logPowIdentityConcrete 
356832     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.98ms 
356833     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logPositive.proof 
356834     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 70.5ns 
356834     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
359137     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.3s 
359138     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logPositive 
359905     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logPositive 
359923     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 15.17ms 
359925     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logPositiveConcrete.proof 
359925     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 89.2ns 
359926     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
362286     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.36s 
362286     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logPositiveConcrete 
363015     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logPositiveConcrete 
363020     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 513.71ns 
363022     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logMono.proof 
363022     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 84ns 
363022     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
365354     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.33s 
365354     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logMono 
366096     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logMono 
366137     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 36.06ms 
366138     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logMonoConcrete.proof 
366138     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 94.6ns 
366139     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
368481     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.34s 
368482     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logMonoConcrete 
369214     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logMonoConcrete 
369218     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.75ms 
369219     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powLogLess.proof 
369219     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 75.6ns 
369220     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
371549     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.33s 
371549     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powLogLess 
372308     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powLogLess 
372330     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 19.01ms 
372333     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powLogMore2.proof 
372333     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 233.4ns 
372334     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
374692     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.36s 
374692     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powLogMore2 
375458     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powLogMore2 
375480     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 19.1ms 
375481     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logLessThanPow.proof 
375481     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 99.2ns 
375482     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
377886     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.4s 
377886     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logLessThanPow 
378656     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logLessThanPow 
378680     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 20.93ms 
378681     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logLessThanPowConcrete.proof 
378681     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 83.3ns 
378682     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
380978     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.3s 
380978     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logLessThanPowConcrete 
381732     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logLessThanPowConcrete 
381734     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 547.01ns 
381735     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logSqueeze.proof 
381735     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 70.3ns 
381736     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
384055     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.32s 
384055     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logSqueeze 
384811     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logSqueeze 
384816     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.85ms 
384818     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/booleanRules/Taclet_ifthenelse_equals.proof 
384818     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 67.1ns 
384819     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
387176     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.36s 
387177     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: ifthenelse_equals 
387935     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: ifthenelse_equals 
387938     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.24ms 
387939     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/booleanRules/Taclet_ifthenelse_equals_1.proof 
387939     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 79.8ns 
387940     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
390230     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.29s 
390230     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: ifthenelse_equals_1 
390987     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: ifthenelse_equals_1 
390990     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 824.81ns 
390992     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/booleanRules/Taclet_ifthenelse_equals_2.proof 
390993     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 223.9ns 
390994     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
393335     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.34s 
393335     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: ifthenelse_equals_2 
394072     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: ifthenelse_equals_2 
394074     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 888.51ns 
394076     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/locSet/Taclet_disjointWithSingleton1.proof 
394076     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 67.9ns 
394076     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
396414     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.34s 
396415     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: disjointWithSingleton1 
397153     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: disjointWithSingleton1 
397156     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.68ms 
397158     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/locSet/Taclet_disjointWithSingleton2.proof 
397158     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 127.3ns 
397159     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
399508     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.35s 
399508     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: disjointWithSingleton2 
400271     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: disjointWithSingleton2 
400274     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.4ms 
400275     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/locSet/Taclet_disjointArrayRanges.proof 
400275     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 57.3ns 
400276     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
402592     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.32s 
402592     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: disjointArrayRanges 
403362     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: disjointArrayRanges 
403373     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 7.84ms 
403374     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/locSet/Taclet_disjointArrayRangeAllFields1.proof 
403375     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 74.5ns 
403375     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
405739     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.36s 
405739     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: disjointArrayRangeAllFields1 
406499     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: disjointArrayRangeAllFields1 
406512     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 10.83ms 
406514     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/locSet/Taclet_disjointArrayRangeAllFields2.proof 
406514     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 74.5ns 
406515     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
408835     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.32s 
408835     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: disjointArrayRangeAllFields2 
409599     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: disjointArrayRangeAllFields2 
409610     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 9.41ms 
409614     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqSelfDefinition.proof 
409614     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 248ns 
409615     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
411962     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.35s 
411963     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqSelfDefinition 
412711     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqSelfDefinition 
412730     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 16.06ms 
412731     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqOutsideValue.proof 
412731     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 92.9ns 
412732     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
415073     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.34s 
415073     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqOutsideValue 
415825     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqOutsideValue 
415833     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 6.04ms 
415834     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_castedGetAny.proof 
415834     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 79.8ns 
415835     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
418174     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.34s 
418174     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: castedGetAny 
418944     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: castedGetAny 
418951     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.63ms 
418952     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqGetAlphaCast.proof 
418952     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 67ns 
418953     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
421262     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.31s 
421263     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqGetAlphaCast 
422043     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqGetAlphaCast 
422045     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 905.02ns 
422047     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqSingleton.proof 
422047     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 76.8ns 
422048     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
424357     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.31s 
424357     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqSingleton 
425121     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqSingleton 
425123     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.35ms 
425125     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqSingletonConcrete.proof 
425125     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 95.4ns 
425126     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
427438     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.31s 
427438     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqSingletonConcrete 
428171     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqSingletonConcrete 
428173     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 774.81ns 
428174     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqConcat.proof 
428174     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 66.6ns 
428175     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
430470     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.29s 
430470     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqConcat 
431225     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqConcat 
431236     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 8.6ms 
431237     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqSub.proof 
431237     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 62.3ns 
431238     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
433558     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.32s 
433558     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqSub 
434316     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqSub 
434320     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.32ms 
434321     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqReverse.proof 
434321     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 68.5ns 
434322     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
436590     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.27s 
436590     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqReverse 
437345     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqReverse 
437352     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.63ms 
437353     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqEmpty.proof 
437353     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 73.8ns 
437354     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
439646     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.29s 
439646     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqEmpty 
440382     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqEmpty 
440384     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 735.01ns 
440386     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqSingleton.proof 
440386     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 61.7ns 
440386     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
442683     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.3s 
442683     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqSingleton 
443439     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqSingleton 
443441     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 605.01ns 
443442     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqConcat.proof 
443443     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 53.7ns 
443443     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
445712     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.27s 
445712     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqConcat 
446470     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqConcat 
446474     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.03ms 
446476     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqSub.proof 
446476     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 224.8ns 
446477     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
448749     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.27s 
448749     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqSub 
449505     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqSub 
449508     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.29ms 
449509     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqReverse.proof 
449509     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 78.3ns 
449510     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
451805     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.29s 
451805     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqReverse 
452537     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqReverse 
452540     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.45ms 
452542     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_equalityToSeqGetAndSeqLenLeft.proof 
452542     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 56.5ns 
452542     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
454830     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.29s 
454830     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: equalityToSeqGetAndSeqLenLeft 
455586     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: equalityToSeqGetAndSeqLenLeft 
455589     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.2ms 
455590     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_equalityToSeqGetAndSeqLenRight.proof 
455590     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 53.6ns 
455591     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
457868     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.28s 
457868     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: equalityToSeqGetAndSeqLenRight 
458627     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: equalityToSeqGetAndSeqLenRight 
458632     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.53ms 
458633     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqSingletonEQ.proof 
458633     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 56.9ns 
458634     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
460935     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.3s 
460935     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqSingletonEQ 
461672     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqSingletonEQ 
461674     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.26ms 
461676     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqConcatEQ.proof 
461676     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 69.7ns 
461676     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
463981     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.3s 
463981     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqConcatEQ 
464739     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqConcatEQ 
464749     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 8.14ms 
464750     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqSubEQ.proof 
464750     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 79.3ns 
464751     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
467030     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.28s 
467030     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqSubEQ 
467788     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqSubEQ 
467790     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 656.41ns 
467791     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqReverseEQ.proof 
467791     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 65.5ns 
467792     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
470088     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.3s 
470088     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqReverseEQ 
470822     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqReverseEQ 
470829     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 5.22ms 
470830     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqEmptyEQ.proof 
470831     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 79.7ns 
470831     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
473131     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.3s 
473131     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqEmptyEQ 
473889     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqEmptyEQ 
473891     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 868.11ns 
473893     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqSingletonEQ.proof 
473893     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 51.9ns 
473893     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
476167     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.27s 
476167     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqSingletonEQ 
476924     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqSingletonEQ 
476926     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 739.11ns 
476927     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqConcatEQ.proof 
476927     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 51.6ns 
476928     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
479218     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.29s 
479218     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqConcatEQ 
479975     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqConcatEQ 
479982     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.32ms 
479984     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqSubEQ.proof 
479984     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 196.4ns 
479985     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
482262     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.28s 
482263     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqSubEQ 
483017     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqSubEQ 
483019     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.46ms 
483021     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqReverseEQ.proof 
483021     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 63.5ns 
483021     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
485308     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.29s 
485308     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqReverseEQ 
486042     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqReverseEQ 
486045     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.89ms 
486047     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqDefEQ.proof 
486047     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 60.3ns 
486047     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
488329     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.28s 
488330     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqDefEQ 
489087     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqDefEQ 
489090     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.97ms 
489092     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqDefEQ.proof 
489092     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 59.1ns 
489092     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
491358     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.27s 
491358     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqDefEQ 
492118     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqDefEQ 
492123     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.04ms 
492124     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqConcatWithSeqEmpty1.proof 
492124     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 69.9ns 
492125     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
494413     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.29s 
494413     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqConcatWithSeqEmpty1 
495166     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqConcatWithSeqEmpty1 
495180     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 11.54ms 
495181     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqConcatWithSeqEmpty2.proof 
495181     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 53.2ns 
495182     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
497452     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.27s 
497452     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqConcatWithSeqEmpty2 
498211     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqConcatWithSeqEmpty2 
498226     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 12.85ms 
498227     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqReverseOfSeqEmpty.proof 
498227     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 82.7ns 
498228     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
500517     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.29s 
500517     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqReverseOfSeqEmpty 
501273     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqReverseOfSeqEmpty 
501283     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 7.93ms 
501284     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_subSeqComplete.proof 
501284     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 77.4ns 
501285     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
503551     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.27s 
503551     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: subSeqComplete 
504307     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: subSeqComplete 
504317     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 8.31ms 
504318     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_subSeqTailR.proof 
504318     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 64.1ns 
504319     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
506600     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.28s 
506600     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: subSeqTailR 
507354     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: subSeqTailR 
507378     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 21.67ms 
507380     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_subSeqTailL.proof 
507380     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 82.2ns 
507380     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
509650     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.27s 
509650     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: subSeqTailL 
510408     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: subSeqTailL 
510432     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 21.52ms 
510433     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_subSeqTailEQR.proof 
510433     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 60.7ns 
510434     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
512715     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.28s 
512715     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: subSeqTailEQR 
513472     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: subSeqTailEQR 
513494     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 20.11ms 
513495     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_subSeqTailEQL.proof 
513495     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 80.6ns 
513496     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
515766     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.27s 
515766     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: subSeqTailEQL 
516522     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: subSeqTailEQL 
516536     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 11.68ms 
516537     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDef_split.proof 
516537     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 73.3ns 
516538     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
518830     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.29s 
518830     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_split 
519585     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDef_split 
519613     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 25.34ms 
519614     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDef_induction_upper.proof 
519614     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 68.5ns 
519615     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
521884     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.27s 
521885     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_induction_upper 
522639     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDef_induction_upper 
522684     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 41.2ms 
522685     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDef_induction_upper_concrete.proof 
522685     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 73.9ns 
522686     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
524988     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.3s 
524988     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_induction_upper_concrete 
525748     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDef_induction_upper_concrete 
525784     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 33.38ms 
525787     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDef_induction_lower.proof 
525787     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 211.1ns 
525788     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
528076     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.29s 
528076     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_induction_lower 
528809     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDef_induction_lower 
528877     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 64.56ms 
528878     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDef_induction_lower_concrete.proof 
528878     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 73.2ns 
528879     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
531146     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.27s 
531146     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_induction_lower_concrete 
531903     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDef_induction_lower_concrete 
531945     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 38.38ms 
531946     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDef_split_in_three.proof 
531946     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 72.7ns 
531947     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
534238     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.29s 
534238     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_split_in_three 
534996     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDef_split_in_three 
535107     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 104.5ms 
535108     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDef_empty.proof 
535108     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 66ns 
535109     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
537415     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.31s 
537415     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_empty 
538149     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDef_empty 
538156     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 5.53ms 
538158     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDef_one_summand.proof 
538158     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 57.2ns 
538158     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
540445     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.29s 
540445     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_one_summand 
541198     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDef_one_summand 
541205     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 5.41ms 
541207     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDef_lower_equals_upper.proof 
541207     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 66.5ns 
541207     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
543507     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.3s 
543507     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_lower_equals_upper 
544263     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDef_lower_equals_upper 
544267     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.37ms 
544269     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDefOfSeq.proof 
544269     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 62.1ns 
544269     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
546540     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.27s 
546540     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDefOfSeq 
547293     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDefOfSeq 
547311     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 14.34ms 
547312     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqSelfDefinitionEQ2.proof 
547312     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 62.9ns 
547313     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
549597     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.28s 
549597     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqSelfDefinitionEQ2 
550354     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqSelfDefinitionEQ2 
550364     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 8.28ms 
550365     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_indexOfSeqSingleton.proof 
550365     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 65ns 
550366     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
552661     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.3s 
552662     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: indexOfSeqSingleton 
553415     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: indexOfSeqSingleton 
553418     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.66ms 
553419     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_indexOfSeqConcatFirst.proof 
553419     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 89.6ns 
553420     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
555690     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.27s 
555690     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: indexOfSeqConcatFirst 
556446     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: indexOfSeqConcatFirst 
556462     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 13.65ms 
556463     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_indexOfSeqConcatSecond.proof 
556463     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 77.5ns 
556464     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
558746     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.28s 
558746     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: indexOfSeqConcatSecond 
559500     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: indexOfSeqConcatSecond 
559516     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 13.07ms 
559517     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_indexOfSeqSub.proof 
559517     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 68.5ns 
559518     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
561806     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.29s 
561806     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: indexOfSeqSub 
562561     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: indexOfSeqSub 
562579     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 15.38ms 
562580     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfArray2seq.proof 
562580     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 54.8ns 
562581     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
564853     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.27s 
564853     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfArray2seq 
565606     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfArray2seq 
565610     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.14ms 
565611     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getAnyOfArray2seq.proof 
565611     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 60.2ns 
565612     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
567897     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.29s 
567897     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getAnyOfArray2seq 
568653     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getAnyOfArray2seq 
568656     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.01ms 
568657     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfArray2seq.proof 
568657     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 55.3ns 
568658     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
570942     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.28s 
570942     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfArray2seq 
571696     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfArray2seq 
571702     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.42ms 
571703     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_getAnyOfNPermInv.proof 
571703     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 49.9ns 
571704     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
573995     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.29s 
573995     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getAnyOfNPermInv 
574729     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getAnyOfNPermInv 
574736     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.69ms 
574737     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqNPermRange.proof 
574737     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 53.3ns 
574738     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
577028     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.29s 
577028     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqNPermRange 
577783     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqNPermRange 
577852     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 63.37ms 
577853     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermTrans.proof 
577853     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 89.3ns 
577854     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
580150     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.3s 
580150     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermTrans 
580911     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermTrans 
580937     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 23.36ms 
580938     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermRefl.proof 
580938     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 69.4ns 
580939     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
583235     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.3s 
583235     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermRefl 
583995     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermRefl 
584017     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 19.17ms 
584018     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermSplit.proof 
584018     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 76.6ns 
584019     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
586321     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.3s 
586321     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermSplit 
587080     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermSplit 
587082     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 270.7ns 
587083     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqNPermRight.proof 
587083     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 53.2ns 
587084     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
589383     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.3s 
589383     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqNPermRight 
590122     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqNPermRight 
590353     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 219.95ms 
590355     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermFromSwap.proof 
590355     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 130.2ns 
590356     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
592649     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.29s 
592649     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermFromSwap 
593383     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermFromSwap 
593431     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 43.26ms 
593432     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermTransAlt0.proof 
593433     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 126.7ns 
593433     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
595713     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.28s 
595713     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermTransAlt0 
596469     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermTransAlt0 
596471     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 371.4ns 
596473     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermTransAlt1.proof 
596474     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 227.5ns 
596474     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
598755     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.28s 
598755     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermTransAlt1 
599509     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermTransAlt1 
599511     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 336.2ns 
599512     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermTransAlt2.proof 
599512     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 70.1ns 
599513     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
601789     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.28s 
601789     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermTransAlt2 
602544     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermTransAlt2 
602546     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 337.2ns 
602547     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermTransAlt3.proof 
602547     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 55.4ns 
602548     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
604839     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.29s 
604839     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermTransAlt3 
605596     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermTransAlt3 
605598     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 495.81ns 
605600     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermForall.proof 
605600     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 73.8ns 
605600     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
607885     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.28s 
607885     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermForall 
608641     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermForall 
608742     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 99ms 
608745     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermExists.proof 
608745     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 247.1ns 
608746     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
611066     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.32s 
611067     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermExists 
611828     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermExists 
611877     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 46.56ms 
611878     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm2/Taclet_schiffl_lemma_2.proof 
611879     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 69.6ns 
611880     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
614201     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.32s 
614202     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: schiffl_lemma_2 
614963     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: schiffl_lemma_2 
614964     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.1ns 
614989     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 1: 'macro split-prop' 
615027     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 2: 'rule allRight' 
615044     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 3: 'rule allRight' 
615048     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 4: 'macro split-prop' 
615053     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 5: 'rule 'seqPermDefLeft'' 
615056     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 6: 'rule 'andLeft'' 
615057     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 7: 'rule 'exLeft'' 
615059     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 8: 'macro split-prop' 
615062     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 9: 'rule  seqNPermRange' 
615064     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 10: 'instantiate var=iv with='v_x_0' occ=1' 
615066     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 11: 'rule impLeft' 
615067     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 12: 'tryclose branch' 
615230     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 13: 'rule andLeft' 
615232     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 14: 'rule andLeft' 
615233     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 15: 'instantiate var=iv with='v_y_0' occ=1' 
615234     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 16: 'rule impLeft' 
615235     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 17: 'tryclose branch' 
615364     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 18: 'rule andLeft' 
615365     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 19: 'rule andLeft' 
615369     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 20: 'rule seqNPermDefLeft' 
615371     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 21: 'instantiate var=iv with='v_x_0' occ=2' 
615373     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 22: 'rule impLeft' 
615375     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 23: 'tryclose branch' 
615572     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 24: 'rule exLeft' 
615575     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 25: 'rule andLeft' 
615576     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 26: 'rule andLeft' 
615577     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 27: 'instantiate hide var=iv with='v_y_0' occ=2' 
615578     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 28: 'rule impLeft' 
615581     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 29: 'tryclose branch' 
615719     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 30: 'rule exLeft' 
615721     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 31: 'rule andLeft' 
615722     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 32: 'rule andLeft' 
615723     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 33: 'instantiate var=iv with='jv_0' occ=1' 
615724     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 34: 'rule impLeft' 
615725     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 35: 'tryclose branch' 
615733     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 36: 'rule andLeft' 
615734     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 37: 'rule andLeft' 
615735     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 38: 'rule castAdd formula='s_0[jv_0] = v_x_0' occ=0' 
615738     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 39: 'instantiate hide var=iv with='jv_1' occ=1' 
615740     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 40: 'rule impLeft' 
615741     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 41: 'tryclose branch' 
615750     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 42: 'rule andLeft' 
615752     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 43: 'rule andLeft' 
615753     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 44: 'rule castAdd formula='s_0[jv_1] = v_y_0' occ=0' 
615754     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 45: 'instantiate var=iv  with='v_x_0'' 
615755     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 46: 'rule impLeft' 
615756     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 47: 'tryclose branch' 
615921     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 48: 'instantiate var=iv  with='v_y_0'' 
615922     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 49: 'rule impLeft' 
615924     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 50: 'tryclose branch' 
616046     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 51: 'cut 'v_x_0 = v_y_0'' 
616048     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)'' 
616050     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 53: 'rule andRight' 
616052     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 54: 'rule andRight' 
616053     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 55: 'rule andRight' 
616055     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 56: 'rule andRight' 
616056     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 57: 'rule lenOfSwap' 
616058     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 58: 'tryclose branch' 
616062     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 59: 'rule seqNPermSwapNPerm' 
616064     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 60: 'instantiate hide var='iv' with='v_x_0' occ=1' 
616065     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 61: 'instantiate hide var='jv' with='jv_0'' 
616066     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 62: 'rule impLeft' 
616067     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 63: 'tryclose branch' 
616180     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 64: 'tryclose branch' 
616184     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 65: 'rule allRight' 
616186     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 66: 'rule impRight' 
616187     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 67: 'rule andLeft' 
616188     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 68: 'instantiate var=iv with='v_iv_0'' 
616189     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 69: 'rule impLeft' 
616191     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 70: 'tryclose branch' 
616325     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 71: 'rule getOfSwap' 
616327     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 72: 'rule ifthenelse_negated' 
616328     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 73: 'rule ifthenelse_split occ=0' 
616330     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 74: 'rule andLeft' 
616330     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 75: 'rule andLeft' 
616331     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 76: 'rule andLeft' 
616332     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 77: 'rule ifthenelse_split occ=0' 
616334     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 78: 'tryclose branch' 
616436     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 79: 'rule ifthenelse_split occ=0' 
616438     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 80: 'tryclose branch' 
616571     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 81: 'tryclose branch' 
616575     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 82: 'tryclose branch' 
616582     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 83: 'rule getOfSwap' 
616583     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 84: 'rule ifthenelse_negated' 
616584     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 85: 'rule ifthenelse_split occ=0' 
616586     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 86: 'rule andLeft' 
616589     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 87: 'rule andLeft' 
616589     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 88: 'rule andLeft' 
616590     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 89: 'rule ifthenelse_split occ=0' 
616591     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 90: 'tryclose branch' 
616600     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 91: 'tryclose branch' 
616606     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 92: 'tryclose branch' 
616709     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 93: 'rule getOfSwap' 
616710     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 94: 'rule ifthenelse_negated' 
616712     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 95: 'rule ifthenelse_split occ=0' 
616714     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 96: 'rule andLeft' 
616714     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 97: 'rule andLeft' 
616715     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 98: 'rule andLeft' 
616715     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 99: 'rule ifthenelse_split occ=0' 
616717     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 100: 'tryclose branch' 
616771     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 101: 'tryclose branch' 
616791     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 102: 'tryclose branch' 
616907     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 103: 'cut '(int)s_0[v_x_0] = (int)s_0[v_y_0]'' 
616909     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 104: 'rule seqNPermInjective' 
616911     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 105: 'instantiate hide var=iv with='v_x_0'' 
616912     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 106: 'instantiate hide var=jv with='v_y_0'' 
616913     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 107: 'rule impLeft' 
616914     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 108: 'tryclose branch' 
617052     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 109: 'tryclose branch' 
617057     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 110: 'cut '(int)s_0[v_x_0] = v_x_0'' 
617060     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)'' 
617061     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 112: 'rule andRight' 
617063     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 113: 'rule andRight' 
617064     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 114: 'rule andRight' 
617065     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 115: 'rule andRight' 
617065     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 116: 'tryclose branch' 
617075     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 117: 'rule seqNPermSwapNPerm' 
617080     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 118: 'instantiate hide var=iv with='v_y_0'' 
617082     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 119: 'instantiate hide var=jv with='jv_1'' 
617082     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 120: 'tryclose branch' 
617174     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 121: 'rule allRight' 
617176     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 122: 'rule impRight' 
617177     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 123: 'rule andLeft' 
617178     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 124: 'instantiate var=iv with='v_iv_0'' 
617179     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 125: 'rule impLeft' 
617180     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 126: 'tryclose branch' 
617281     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 127: 'rule getOfSwap' 
617283     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 128: 'rule ifthenelse_negated' 
617284     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 129: 'rule ifthenelse_split occ=0' 
617286     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 130: 'rule andLeft' 
617286     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 131: 'rule andLeft' 
617287     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 132: 'rule andLeft' 
617287     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 133: 'rule ifthenelse_split occ=0' 
617289     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 134: 'tryclose branch' 
617374     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 135: 'rule ifthenelse_split occ=0' 
617376     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 136: 'tryclose branch' 
617469     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 137: 'instantiate var=iv with='v_y_0'' 
617470     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 138: 'rule impLeft' 
617471     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 139: 'tryclose branch' 
617479     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 140: 'tryclose branch' 
617483     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 141: 'tryclose branch' 
617488     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 142: 'tryclose branch' 
617616     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 143: 'rule getOfSwap' 
617617     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 144: 'rule ifthenelse_negated' 
617618     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 145: 'rule ifthenelse_split occ=0' 
617619     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 146: 'tryclose branch' 
617630     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 147: 'tryclose branch' 
617711     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 148: 'tryclose branch' 
621202     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 149: 'cut  '(int)s_0[v_y_0] = v_y_0'' 
621203     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)'' 
621208     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 151: 'rule andRight' 
621209     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 152: 'rule andRight' 
621209     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 153: 'rule andRight' 
621210     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 154: 'rule andRight' 
621210     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 155: 'tryclose branch' 
621218     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 156: 'rule seqNPermSwapNPerm' 
621219     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 157: 'instantiate hide var=iv with='v_x_0'' 
621220     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 158: 'instantiate hide var=jv with='jv_0'' 
621221     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 159: 'rule impLeft' 
621221     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 160: 'tryclose branch' 
621315     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 161: 'tryclose branch' 
621319     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 162: 'rule allRight' 
621320     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 163: 'rule impRight' 
621320     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 164: 'rule andLeft' 
621321     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 165: 'instantiate var=iv with='v_iv_0'' 
621322     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 166: 'rule impLeft' 
621322     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 167: 'tryclose branch' 
621417     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 168: 'rule getOfSwap' 
621419     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 169: 'rule ifthenelse_negated' 
621419     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 170: 'rule ifthenelse_split occ=0' 
621420     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 171: 'rule andLeft' 
621421     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 172: 'rule andLeft' 
621421     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 173: 'rule andLeft' 
621422     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 174: 'rule ifthenelse_split occ=0' 
621423     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 175: 'tryclose branch' 
621498     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 176: 'rule ifthenelse_split occ=0' 
621500     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 177: 'tryclose branch' 
621572     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 178: 'tryclose branch' 
621576     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 179: 'tryclose branch' 
621580     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 180: 'rule getOfSwap' 
621581     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 181: 'rule ifthenelse_negated' 
621582     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 182: 'rule ifthenelse_split occ=0' 
621582     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 183: 'tryclose branch' 
621592     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 184: 'tryclose branch' 
621671     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 185: 'rule getOfSwap' 
621672     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 186: 'rule ifthenelse_negated' 
621673     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 187: 'rule ifthenelse_split occ=0' 
621674     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 188: 'tryclose branch' 
621747     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 189: 'tryclose branch' 
621756     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 190: 'cut '(int)s_0[v_x_0]=v_y_0'' 
621756     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)'' 
621758     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 192: 'rule andRight' 
621759     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 193: 'rule andRight' 
621759     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 194: 'rule andRight' 
621760     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 195: 'rule andRight' 
621760     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 196: 'tryclose branch' 
621771     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 197: 'rule seqNPermSwapNPerm' 
621772     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 198: 'instantiate hide var=iv with='jv_0'' 
621773     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 199: 'instantiate hide var=jv with='v_x_0'' 
621773     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 200: 'rule impLeft' 
621774     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 201: 'tryclose branch' 
621861     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 202: 'rule seqNPermSwapNPerm formula='seqNPerm(seqSwap(s_0, jv_0, v_x_0))'' 
621863     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 203: 'instantiate hide var=iv with='jv_0'' 
621864     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 204: 'instantiate hide var=jv with='v_y_0'' 
621864     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 205: 'rule impLeft' 
621865     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 206: 'tryclose branch' 
621955     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 207: 'tryclose branch' 
621960     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 208: 'rule allRight' 
621961     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 209: 'rule impRight' 
621961     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 210: 'rule andLeft' 
621962     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 211: 'instantiate var=iv with='v_iv_0'' 
621962     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 212: 'rule impLeft' 
621963     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 213: 'tryclose branch' 
622061     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 214: 'rule getOfSwap' 
622063     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 215: 'rule ifthenelse_negated' 
622063     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 216: 'rule ifthenelse_split occ=0' 
622065     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 217: 'rule andLeft' 
622065     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 218: 'rule andLeft' 
622066     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 219: 'rule andLeft' 
622066     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 220: 'rule ifthenelse_split occ=0' 
622067     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 221: 'rule getOfSwap' 
622068     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 222: 'rule ifthenelse_negated' 
622068     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 223: 'rule ifthenelse_split occ=0' 
622069     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 224: 'rule andLeft' 
622070     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 225: 'rule andLeft' 
622070     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 226: 'rule andLeft' 
622070     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 227: 'rule ifthenelse_split occ=0' 
622071     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 228: 'tryclose branch' 
622201     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 229: 'rule ifthenelse_split occ=0' 
622202     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 230: 'tryclose branch' 
622208     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 231: 'tryclose branch' 
622284     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 232: 'tryclose branch' 
622364     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 233: 'rule ifthenelse_split' 
622365     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 234: 'rule getOfSwap' 
622366     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 235: 'rule ifthenelse_negated' 
622367     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 236: 'rule ifthenelse_split occ=0' 
622368     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 237: 'rule andLeft' 
622368     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 238: 'rule andLeft' 
622368     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 239: 'rule andLeft' 
622369     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 240: 'rule ifthenelse_split occ=0' 
622370     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 241: 'tryclose branch' 
622455     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 242: 'tryclose branch' 
622460     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 243: 'tryclose branch' 
622549     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 244: 'rule getOfSwap' 
622550     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 245: 'rule ifthenelse_negated' 
622551     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 246: 'rule ifthenelse_split occ=0' 
622552     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 247: 'rule andLeft' 
622552     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 248: 'rule andLeft' 
622552     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 249: 'rule andLeft' 
622553     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 250: 'rule ifthenelse_split occ=0' 
622553     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 251: 'tryclose branch' 
622558     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 252: 'rule ifthenelse_split occ=0' 
622559     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 253: 'tryclose branch' 
622638     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 254: 'tryclose branch' 
622643     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 255: 'tryclose branch' 
622648     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 256: 'tryclose branch' 
622747     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 257: 'rule getOfSwap' 
622748     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 258: 'rule ifthenelse_negated' 
622749     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 259: 'rule ifthenelse_split occ=0' 
622750     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 260: 'rule andLeft' 
622750     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 261: 'rule andLeft' 
622751     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 262: 'rule andLeft' 
622751     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 263: 'rule ifthenelse_split occ=0' 
622752     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 264: 'tryclose branch' 
622806     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 265: 'rule ifthenelse_split occ=0' 
622807     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 266: 'rule getOfSwap' 
622808     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 267: 'rule ifthenelse_negated' 
622808     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 268: 'rule ifthenelse_split occ=0' 
622809     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 269: 'tryclose branch' 
622815     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 270: 'tryclose branch' 
622820     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 271: 'tryclose branch' 
622936     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 272: 'tryclose branch' 
623024     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 273: 'rule getOfSwap' 
623025     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 274: 'rule ifthenelse_negated' 
623025     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 275: 'rule ifthenelse_split occ=0' 
623026     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 276: 'tryclose branch' 
623193     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 277: 'tryclose branch' 
623281     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 278: 'cut 'int::seqGet(s_0, v_y_0)=v_x_0'' 
623281     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 279: 'tryclose branch' 
626368     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 280: 'rule seqNPermSwapNPerm' 
626373     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 281: 'instantiate hide var=iv with='jv_1'' 
626374     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 282: 'instantiate hide var=jv with='v_y_0'' 
626375     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 283: 'rule impLeft' 
626376     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 284: 'tryclose branch' 
626493     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 285: 'rule seqNPermSwapNPerm formula='seqNPerm(seqSwap(s_0,jv_1,v_y_0))'' 
626495     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 286: 'instantiate hide var=iv with='jv_1'' 
626497     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 287: 'instantiate hide var=jv with='v_x_0'' 
626497     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 288: 'rule impLeft' 
626498     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 289: 'tryclose branch' 
626607     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 290: 'tryclose branch' 
629581     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 291: 'tryclose branch' 
632784     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 292: 'rule seqNPermSwapNPerm formula='seqNPerm(s_0)'' 
632788     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 293: 'instantiate hide var=iv with='v_x_0'' 
632789     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 294: 'instantiate hide var=jv with='jv_0'' 
632790     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 295: 'rule impLeft' 
632790     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 296: 'tryclose branch' 
632905     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 297: 'rule seqNPermSwapNPerm formula='seqNPerm(seqSwap(s_0,v_x_0,jv_0))'' 
632906     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 298: 'instantiate hide var=iv with='v_y_0'' 
632908     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 299: 'instantiate hide var=jv with='jv_1'' 
632909     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)' ...' 
632911     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 301: 'tryclose branch' 
634086     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm2/Taclet_schiffl_thm_1.proof 
634086     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 86.1ns 
634087     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
636453     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.37s 
636453     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: schiffl_thm_1 
637237     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: schiffl_thm_1 
637239     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 7ns 
637239     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 1: 'macro split-prop' 
637245     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 2: 'rule schiffl_lemma_2 formula='seqPerm(f_s, f_t)'' 
637256     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 3: 'instantiate hide var=x with='f_x'' 
637258     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 4: 'instantiate hide var=y with='f_y'' 
637260     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 5: 'rule impLeft' 
637261     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 6: 'tryclose branch' 
637264     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 7: 'rule exLeft' 
637266     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 8: 'macro split-prop' 
637268     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 9: 'rule seqPermDef occ=1' 
637271     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 10: 'rule andRight' 
637271     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 11: 'tryclose branch' 
637279     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 12: 'instantiate hide var=s with='r_0'' 
637280     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 13: 'rule andRight' 
637281     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 14: 'tryclose branch' 
637323     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 15: 'rule allRight' 
637324     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 16: 'rule impRight' 
637325     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 17: 'instantiate hide var=iv with='iv_0'' 
637325     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 18: 'rule impLeft' 
637326     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 19: 'tryclose branch' 
637387     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 20: 'rule andLeft' 
637387     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 21: 'rule seqNPermRange' 
637389     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 22: 'instantiate hide var=iv with='iv_0'' 
637389     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 23: 'rule impLeft' 
637390     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 24: 'tryclose branch' 
637393     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 25: 'rule andLeft' 
637394     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 26: 'rule andLeft' 
637394     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 27: 'rule seqNPermRange' 
637395     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 28: 'instantiate hide var=iv with='f_x'' 
637396     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 29: 'rule impLeft' 
637397     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 30: 'tryclose branch' 
637474     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 31: 'rule andLeft' 
637475     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 32: 'rule andLeft' 
637476     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 33: 'rule seqNPermRange' 
637477     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 34: 'instantiate hide var=iv with='f_y'' 
637478     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 35: 'rule impLeft' 
637478     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 36: 'tryclose branch' 
637558     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 37: 'rule andLeft' 
637559     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 38: 'rule andLeft' 
637560     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 39: 'rule getOfSeqDef occ=0' 
637560     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 40: 'rule getOfSeqDef' 
637561     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 41: 'rule ifthenelse_split occ=0' 
637562     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 42: 'rule andLeft occ=0' 
637562     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 43: 'rule sub_zero_2 occ=0' 
637563     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 44: 'rule ifthenelse_split occ=2' 
637564     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 45: 'rule andLeft' 
637564     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 46: 'rule sub_zero_2 occ=0' 
637565     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 47: 'rule add_zero_right occ=0' 
637565     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 48: 'rule add_zero_right occ=0' 
637566     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 49: 'rule add_zero_right occ=0' 
637567     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 50: 'rule add_zero_right occ=0' 
637567     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 51: 'rule add_zero_right occ=0' 
637568     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 52: 'rule add_zero_right occ=0' 
637568     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 53: 'rule ifthenelse_split occ=0' 
637569     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 54: 'rule ifthenelse_split occ=0' 
637570     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 55: 'tryclose branch' 
637573     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 56: 'tryclose branch' 
637605     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 57: 'rule ifthenelse_split occ=0' 
637607     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 58: 'tryclose branch' 
637654     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 59: 'rule ifthenelse_split occ=0' 
637655     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 60: 'rule seqNPermInjective' 
637657     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 61: 'instantiate hide var=iv with='iv_0'' 
637658     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 62: 'instantiate hide var=jv with='f_y'' 
637659     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 63: 'rule impLeft' 
637659     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 64: 'tryclose branch' 
637702     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 65: 'tryclose branch' 
637704     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 66: 'rule ifthenelse_split occ=0' 
637705     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 67: 'rule seqNPermInjective' 
637707     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 68: 'instantiate hide var=iv with='iv_0'' 
637708     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 69: 'instantiate hide var=jv with='f_x'' 
637709     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 70: 'rule impLeft' 
637709     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 71: 'tryclose branch' 
637751     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 72: 'tryclose branch' 
637756     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 73: 'tryclose branch' 
637758     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 74: 'tryclose branch' 
637825     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 75: 'tryclose branch' 
637877     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_eqSameSeq.proof 
637878     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 241.1ns 
637879     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
640216     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.34s 
640216     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: eqSameSeq 
640975     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: eqSameSeq 
641030     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 51.55ms