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

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

tests
0

failures
0

ignored
14m16.77s

duration
100%

successful

Tests

Test Method name Duration Result
powPositive data()[100] 4.182s passed
powPositiveConcrete data()[101] 4.208s passed
powGeq1Concrete data()[102] 4.265s passed
pow2InIntLower data()[103] 4.316s passed
pow2InIntUpper data()[104] 4.239s passed
logSelfConcrete data()[105] 4.294s passed
log1Concrete data()[106] 4.181s passed
logProduct data()[107] 4.233s passed
logTimesBaseConcrete data()[108] 4.204s passed
logProdIdentity data()[109] 4.217s passed
moduloByteIsInByte data()[10] 4.423s passed
logProdIdentityConcrete data()[110] 4.195s passed
logPowIdentity data()[111] 4.263s passed
logPowIdentityConcrete data()[112] 4.291s passed
logPositive data()[113] 4.353s passed
logPositiveConcrete data()[114] 4.275s passed
logMono data()[115] 4.328s passed
logMonoConcrete data()[116] 4.356s passed
powLogLess data()[117] 4.292s passed
powLogMore2 data()[118] 4.202s passed
logLessThanPow data()[119] 4.298s passed
moduloCharIsInChar data()[11] 4.299s passed
logLessThanPowConcrete data()[120] 4.300s passed
logSqueeze data()[121] 4.293s passed
ifthenelse_equals data()[122] 4.228s passed
ifthenelse_equals_1 data()[123] 4.274s passed
ifthenelse_equals_2 data()[124] 4.258s passed
disjointWithSingleton1 data()[125] 4.255s passed
disjointWithSingleton2 data()[126] 4.316s passed
disjointArrayRanges data()[127] 4.254s passed
disjointArrayRangeAllFields1 data()[128] 4.253s passed
disjointArrayRangeAllFields2 data()[129] 4.247s passed
div_unique1 data()[12] 4.255s passed
seqSelfDefinition data()[130] 4.180s passed
seqOutsideValue data()[131] 4.138s passed
castedGetAny data()[132] 4.036s passed
seqGetAlphaCast data()[133] 4.022s passed
getOfSeqSingleton data()[134] 4.035s passed
getOfSeqSingletonConcrete data()[135] 4.067s passed
getOfSeqConcat data()[136] 4.045s passed
getOfSeqSub data()[137] 4.074s passed
getOfSeqReverse data()[138] 4.106s passed
lenOfSeqEmpty data()[139] 4.026s passed
div_unique2 data()[13] 4.423s passed
lenOfSeqSingleton data()[140] 3.948s passed
lenOfSeqConcat data()[141] 4.135s passed
lenOfSeqSub data()[142] 4.058s passed
lenOfSeqReverse data()[143] 4.015s passed
equalityToSeqGetAndSeqLenLeft data()[144] 4.060s passed
equalityToSeqGetAndSeqLenRight data()[145] 4.060s passed
getOfSeqSingletonEQ data()[146] 4.006s passed
getOfSeqConcatEQ data()[147] 4.061s passed
getOfSeqSubEQ data()[148] 3.990s passed
getOfSeqReverseEQ data()[149] 4.086s passed
div_exists data()[14] 4.542s passed
lenOfSeqEmptyEQ data()[150] 4.114s passed
lenOfSeqSingletonEQ data()[151] 4.083s passed
lenOfSeqConcatEQ data()[152] 4.067s passed
lenOfSeqSubEQ data()[153] 4.053s passed
lenOfSeqReverseEQ data()[154] 4.052s passed
getOfSeqDefEQ data()[155] 4.078s passed
lenOfSeqDefEQ data()[156] 4.144s passed
seqConcatWithSeqEmpty1 data()[157] 4.228s passed
seqConcatWithSeqEmpty2 data()[158] 4.179s passed
seqReverseOfSeqEmpty data()[159] 4.151s passed
div_one data()[15] 4.275s passed
subSeqComplete data()[160] 4.026s passed
subSeqTailR data()[161] 4.038s passed
subSeqTailL data()[162] 4.111s passed
subSeqTailEQR data()[163] 4.146s passed
subSeqTailEQL data()[164] 4.114s passed
seqDef_split data()[165] 4.137s passed
seqDef_induction_upper data()[166] 4.026s passed
seqDef_induction_upper_concrete data()[167] 4.265s passed
seqDef_induction_lower data()[168] 4.129s passed
seqDef_induction_lower_concrete data()[169] 4.066s passed
jdiv_one data()[16] 4.500s passed
seqDef_split_in_three data()[170] 4.071s passed
seqDef_empty data()[171] 3.974s passed
seqDef_one_summand data()[172] 3.900s passed
seqDef_lower_equals_upper data()[173] 3.993s passed
seqDefOfSeq data()[174] 4.018s passed
seqSelfDefinitionEQ2 data()[175] 4.047s passed
indexOfSeqSingleton data()[176] 4.106s passed
indexOfSeqConcatFirst data()[177] 4.104s passed
indexOfSeqConcatSecond data()[178] 4.120s passed
indexOfSeqSub data()[179] 4.062s passed
div_zero data()[17] 4.488s passed
lenOfArray2seq data()[180] 4.071s passed
getAnyOfArray2seq data()[181] 4.066s passed
getOfArray2seq data()[182] 4.240s passed
getAnyOfNPermInv data()[183] 4.179s passed
seqNPermRange data()[184] 4.225s passed
seqPermTrans data()[185] 4.158s passed
seqPermRefl data()[186] 4.179s passed
seqPermSplit data()[187] 4.162s passed
seqNPermRight data()[188] 4.328s passed
seqPermFromSwap data()[189] 4.160s passed
divResZero1 data()[18] 4.353s passed
seqPermTransAlt0 data()[190] 4.034s passed
seqPermTransAlt1 data()[191] 4.088s passed
seqPermTransAlt2 data()[192] 4.220s passed
seqPermTransAlt3 data()[193] 4.095s passed
seqPermForall data()[194] 4.187s passed
seqPermExists data()[195] 4.165s passed
schiffl_lemma_2 data()[196] 29.264s passed
schiffl_thm_1 data()[197] 5.368s passed
eqSameSeq data()[198] 4.302s passed
divResZero2 data()[19] 4.086s passed
eqTermCut data()[1] 4.938s passed
divResOne1 data()[20] 4.078s passed
divResOne2 data()[21] 4.106s passed
div_cancel1 data()[22] 4.048s passed
div_cancel2 data()[23] 4.211s passed
divAddMultDenom data()[24] 4.309s passed
divMinus data()[25] 4.488s passed
divMinusDenom data()[26] 4.415s passed
divLeastDPos data()[27] 4.269s passed
divLeastDNeg data()[28] 4.192s passed
divGreatestDPos data()[29] 4.200s passed
equivAllRight data()[2] 4.616s passed
divGreatestDNeg data()[30] 4.197s passed
divIncreasingPos data()[31] 4.255s passed
divIncreasingNeg data()[32] 4.153s passed
jdiv_zero data()[33] 4.203s passed
jdivPulloutMinusNum data()[34] 4.146s passed
jdivPulloutMinusDenom data()[35] 4.239s passed
jdiv_uniquePosPos data()[36] 4.233s passed
jdiv_uniquePosNeg data()[37] 4.228s passed
jdiv_uniqueNegPos data()[38] 4.210s passed
jdiv_uniqueNegNeg data()[39] 4.192s passed
irrflConcrete1 data()[3] 4.400s passed
jdivMultDenom1 data()[40] 4.207s passed
jdivMultDenom2 data()[41] 4.255s passed
mod_geZero data()[42] 4.203s passed
mod_lessDenom data()[43] 4.185s passed
jmod_NumPos data()[44] 4.258s passed
jmod_NumNeg data()[45] 4.217s passed
jmod_geZero data()[46] 4.131s passed
jmodNumZero data()[47] 4.211s passed
jmod_pulloutminusNum data()[48] 4.136s passed
jmod_pulloutminusDenom data()[49] 4.025s passed
irrflConcrete2 data()[4] 4.274s passed
jmodUnique1 data()[50] 4.487s passed
jmodUnique2 data()[51] 4.341s passed
intDivRem data()[52] 4.033s passed
jmodjmod data()[53] 4.086s passed
jmodDivisible data()[54] 4.117s passed
jmodDivisibleRep data()[55] 4.017s passed
jdivAddMultDenom data()[56] 4.316s passed
jmodAltZero data()[57] 4.055s passed
jmodAddMultDenomZero data()[58] 4.149s passed
polyDiv_zero data()[59] 4.127s passed
cancel_gtPos data()[5] 4.403s passed
polyMod_ltdivDenom data()[60] 4.150s passed
bsum_empty data()[61] 4.001s passed
bsum_induction_upper data()[62] 4.009s passed
bsum_induction_lower data()[63] 4.000s passed
bsum_num_of_bounds data()[64] 4.198s passed
bsum_num_of_bounds2 data()[65] 4.084s passed
bsum_induction_upper2 data()[66] 4.094s passed
bsum_induction_upper_concrete data()[67] 4.094s passed
bsum_induction_upper_concrete_2 data()[68] 4.177s passed
bsum_induction_upper2_concrete data()[69] 4.212s passed
cancel_gtNeg data()[6] 4.517s passed
bsum_induction_lower_concrete data()[70] 4.141s passed
bsum_induction_lower2 data()[71] 4.185s passed
bsum_induction_lower2_concrete data()[72] 4.114s passed
bsum_positive data()[73] 4.219s passed
bsum_upper_bound data()[74] 4.243s passed
bsum_lower_bound data()[75] 4.218s passed
bsum_positive_lower_bound_element data()[76] 4.200s passed
bsum_sub_same_index data()[77] 4.294s passed
bsum_less_same_index data()[78] 4.373s passed
bsum_equal_except_one_index data()[79] 4.283s passed
moduloIntIsInInt data()[7] 4.328s passed
bsum_num_of_is_max data()[80] 4.276s passed
bsum_num_of_is_max2 data()[81] 4.351s passed
bsum_num_of_is_max3 data()[82] 4.284s passed
bsum_num_of_is_max4 data()[83] 4.376s passed
bsum_num_of_lt_max data()[84] 4.280s passed
bsum_num_of_lt_max2 data()[85] 4.262s passed
bsum_num_of_lt_max3 data()[86] 4.248s passed
bsum_num_of_lt_max4 data()[87] 4.107s passed
bsum_num_of_gt0 data()[88] 4.142s passed
bsum_num_of_gt0_alt data()[89] 4.268s passed
moduloLongIsInLong data()[8] 4.463s passed
bsum_add_concrete data()[90] 4.172s passed
bprod_all_positive data()[91] 4.137s passed
bprod_split data()[92] 4.304s passed
powConcrete0 data()[93] 4.209s passed
powConcrete1 data()[94] 4.155s passed
powSplitFactor data()[95] 4.269s passed
powAdd data()[96] 4.116s passed
powMono data()[97] 4.305s passed
powMonoConcrete data()[98] 4.147s passed
powMonoConcreteRight data()[99] 4.147s passed
moduloShortIsInShort data()[9] 4.302s passed

Standard output

397        INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src/test/resources/testcase/dummyTrue.key 
423        DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 11.98ms 
694        INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
710        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)

1921       DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for Meta 
1923       DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for Meta 
1927       DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for Meta 
1927       DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for Meta 
3957       DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for JavaBigintExpression 
10944      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 10.25s 
11036      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof dummyTrue.key 
11086      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 57.2ns 
11103      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/firstOrder/Taclet_eqTermCut.proof 
11103      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 185.9ns 
11108      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
14813      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.71s 
14818      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: eqTermCut 
15990      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: eqTermCut 
16030      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 25.09ms 
16044      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/firstOrder/Taclet_equivAllRight.proof 
16045      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 137.6ns 
16047      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
19418      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.37s 
19419      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: equivAllRight 
20638      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: equivAllRight 
20656      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 13.93ms 
20664      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_irrflConcrete1.proof 
20664      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 419.4ns 
20666      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
24015      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.35s 
24015      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: irrflConcrete1 
25049      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: irrflConcrete1 
25057      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.84ms 
25061      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_irrflConcrete2.proof 
25061      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 433.1ns 
25063      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
28257      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.19s 
28258      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: irrflConcrete2 
29326      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: irrflConcrete2 
29333      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.83ms 
29337      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_cancel_gtPos.proof 
29338      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 617.4ns 
29339      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
32572      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.23s 
32574      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: cancel_gtPos 
33633      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: cancel_gtPos 
33737      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 99.22ms 
33739      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_cancel_gtNeg.proof 
33739      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 164ns 
33740      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
37142      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.4s 
37142      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: cancel_gtNeg 
38230      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: cancel_gtNeg 
38254      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 20.95ms 
38257      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intRulesIgnoringOF/Taclet_moduloIntIsInInt.proof 
38257      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 119.3ns 
38258      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
41494      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.24s 
41495      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: moduloIntIsInInt 
42578      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: moduloIntIsInInt 
42582      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 847.6ns 
42585      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intRulesIgnoringOF/Taclet_moduloLongIsInLong.proof 
42585      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 348.2ns 
42587      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
45914      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.33s 
45915      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: moduloLongIsInLong 
47041      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: moduloLongIsInLong 
47045      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 773.9ns 
47053      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intRulesIgnoringOF/Taclet_moduloShortIsInShort.proof 
47053      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 660.5ns 
47055      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
50279      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.22s 
50280      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: moduloShortIsInShort 
51346      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: moduloShortIsInShort 
51349      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 714.3ns 
51352      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intRulesIgnoringOF/Taclet_moduloByteIsInByte.proof 
51352      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 214ns 
51353      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
54676      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.32s 
54677      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: moduloByteIsInByte 
55763      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: moduloByteIsInByte 
55767      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 852.7ns 
55775      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intRulesIgnoringOF/Taclet_moduloCharIsInChar.proof 
55775      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 377.2ns 
55778      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
59018      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.24s 
59018      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: moduloCharIsInChar 
60062      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: moduloCharIsInChar 
60070      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.19ms 
60074      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_div_unique1.proof 
60074      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 162.2ns 
60075      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
63228      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.15s 
63228      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: div_unique1 
64272      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: div_unique1 
64326      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 50.13ms 
64328      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_div_unique2.proof 
64329      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 178.8ns 
64330      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
67626      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.3s 
67626      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: div_unique2 
68687      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: div_unique2 
68742      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 51.46ms 
68754      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_div_exists.proof 
68754      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 462.1ns 
68756      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
71935      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.18s 
71936      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: div_exists 
73017      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: div_exists 
73293      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 264.71ms 
73296      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_div_one.proof 
73296      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 118.9ns 
73297      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
76508      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.21s 
76508      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: div_one 
77562      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: div_one 
77569      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.25ms 
77571      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdiv_one.proof 
77572      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 209.6ns 
77575      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
80962      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.39s 
80963      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdiv_one 
82065      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdiv_one 
82069      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.59ms 
82073      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_div_zero.proof 
82074      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 413.3ns 
82077      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
85404      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.33s 
85405      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: div_zero 
86502      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: div_zero 
86558      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 49.22ms 
86561      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divResZero1.proof 
86562      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 353.2ns 
86563      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
89910      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.35s 
89910      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divResZero1 
90889      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divResZero1 
90912      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 18.77ms 
90915      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divResZero2.proof 
90915      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 412.1ns 
90917      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
93995      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.08s 
93996      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divResZero2 
94976      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divResZero2 
94998      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 18.29ms 
95001      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divResOne1.proof 
95003      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 2.12ms 
95008      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
98068      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.06s 
98069      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divResOne1 
99054      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divResOne1 
99077      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 19.54ms 
99080      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divResOne2.proof 
99080      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 302.3ns 
99081      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
102077     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3s 
102077     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divResOne2 
103161     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divResOne2 
103183     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 18.31ms 
103185     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_div_cancel1.proof 
103185     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 223.4ns 
103186     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
106224     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.04s 
106224     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: div_cancel1 
107196     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: div_cancel1 
107231     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 30.79ms 
107233     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_div_cancel2.proof 
107233     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 131.6ns 
107234     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
110354     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.12s 
110354     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: div_cancel2 
111438     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: div_cancel2 
111442     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.5ms 
111444     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divAddMultDenom.proof 
111444     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 143.9ns 
111445     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
114661     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.22s 
114663     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divAddMultDenom 
115686     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divAddMultDenom 
115750     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 57.32ms 
115753     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divMinus.proof 
115754     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 384ns 
115755     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
119076     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.32s 
119078     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divMinus 
120142     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divMinus 
120238     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 87.28ms 
120242     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divMinusDenom.proof 
120242     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 327.4ns 
120243     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
123570     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.33s 
123570     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divMinusDenom 
124576     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divMinusDenom 
124653     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 68.44ms 
124657     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divLeastDPos.proof 
124661     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 3.3ms 
124663     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
127901     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.24s 
127902     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divLeastDPos 
128911     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divLeastDPos 
128923     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 8.88ms 
128925     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divLeastDNeg.proof 
128925     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 109.9ns 
128926     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
132076     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.15s 
132076     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divLeastDNeg 
133096     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divLeastDNeg 
133115     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 16.05ms 
133116     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divGreatestDPos.proof 
133117     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 115.7ns 
133117     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
136242     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.12s 
136242     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divGreatestDPos 
137291     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divGreatestDPos 
137314     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 19.86ms 
137317     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divGreatestDNeg.proof 
137317     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 133.8ns 
137318     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
140454     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.14s 
140454     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divGreatestDNeg 
141501     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divGreatestDNeg 
141512     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 8.27ms 
141514     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divIncreasingPos.proof 
141514     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 95.2ns 
141515     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
144710     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.19s 
144710     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divIncreasingPos 
145756     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divIncreasingPos 
145766     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 8.03ms 
145769     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divIncreasingNeg.proof 
145769     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 289.7ns 
145770     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
148895     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.13s 
148896     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divIncreasingNeg 
149911     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divIncreasingNeg 
149920     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 7.22ms 
149922     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdiv_zero.proof 
149922     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 161.9ns 
149923     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
153108     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.18s 
153108     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdiv_zero 
154119     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdiv_zero 
154124     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.18ms 
154125     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdivPulloutMinusNum.proof 
154126     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 168.4ns 
154127     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
157282     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.15s 
157282     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdivPulloutMinusNum 
158254     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdivPulloutMinusNum 
158269     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 12.28ms 
158271     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdivPulloutMinusDenom.proof 
158271     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 231.3ns 
158273     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
161415     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.14s 
161415     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdivPulloutMinusDenom 
162424     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdivPulloutMinusDenom 
162507     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 76.35ms 
162510     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdiv_uniquePosPos.proof 
162510     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 311.5ns 
162512     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
165680     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.17s 
165681     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdiv_uniquePosPos 
166714     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdiv_uniquePosPos 
166741     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 22.98ms 
166743     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdiv_uniquePosNeg.proof 
166743     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 279.9ns 
166744     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
169925     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.18s 
169925     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdiv_uniquePosNeg 
170937     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdiv_uniquePosNeg 
170968     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 26.83ms 
170972     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdiv_uniqueNegPos.proof 
170973     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 318.6ns 
170975     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
174115     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.14s 
174115     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdiv_uniqueNegPos 
175146     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdiv_uniqueNegPos 
175178     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 27.16ms 
175181     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdiv_uniqueNegNeg.proof 
175181     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 115.1ns 
175182     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
178321     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.14s 
178321     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdiv_uniqueNegNeg 
179349     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdiv_uniqueNegNeg 
179371     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 19.27ms 
179372     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdivMultDenom1.proof 
179372     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 89ns 
179373     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
182490     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.12s 
182490     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdivMultDenom1 
183517     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdivMultDenom1 
183577     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 52.83ms 
183580     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdivMultDenom2.proof 
183580     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 307.9ns 
183582     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
186786     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.2s 
186787     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdivMultDenom2 
187825     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdivMultDenom2 
187833     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.55ms 
187836     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_mod_geZero.proof 
187836     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 91.4ns 
187837     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
191026     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.19s 
191027     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: mod_geZero 
192030     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: mod_geZero 
192036     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.8ms 
192038     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_mod_lessDenom.proof 
192038     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 180.6ns 
192040     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
195232     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.19s 
195233     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: mod_lessDenom 
196209     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: mod_lessDenom 
196222     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 10.1ms 
196223     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmod_NumPos.proof 
196223     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 80.4ns 
196224     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
199396     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.17s 
199396     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmod_NumPos 
200468     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmod_NumPos 
200479     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 9.09ms 
200481     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmod_NumNeg.proof 
200482     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 94.5ns 
200482     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
203653     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.17s 
203654     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmod_NumNeg 
204668     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmod_NumNeg 
204696     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 24.66ms 
204698     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmod_geZero.proof 
204698     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 100.1ns 
204699     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
207796     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.1s 
207796     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmod_geZero 
208815     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmod_geZero 
208827     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 8.49ms 
208828     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmodNumZero.proof 
208828     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 79ns 
208829     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
211974     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.14s 
211975     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmodNumZero 
213034     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmodNumZero 
213038     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.67ms 
213041     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmod_pulloutminusNum.proof 
213041     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 185.1ns 
213042     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
216171     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.13s 
216171     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmod_pulloutminusNum 
217170     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmod_pulloutminusNum 
217175     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.76ms 
217176     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmod_pulloutminusDenom.proof 
217176     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 76.1ns 
217177     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
220230     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.05s 
220230     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmod_pulloutminusDenom 
221194     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmod_pulloutminusDenom 
221200     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.2ms 
221201     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmodUnique1.proof 
221201     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 71.9ns 
221202     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
224541     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.34s 
224541     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmodUnique1 
225568     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmodUnique1 
225685     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 106.91ms 
225688     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmodUnique2.proof 
225688     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 259.4ns 
225690     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
228902     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.21s 
228902     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmodUnique2 
229895     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmodUnique2 
230027     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 120.69ms 
230033     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_intDivRem.proof 
230033     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 279.6ns 
230034     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
233064     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.03s 
233064     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: intDivRem 
234056     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: intDivRem 
234060     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.27ms 
234062     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmodjmod.proof 
234062     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 72.5ns 
234063     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
237079     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.02s 
237080     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmodjmod 
238074     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmodjmod 
238146     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 67.07ms 
238147     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmodDivisible.proof 
238148     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 254.6ns 
238152     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
241182     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.03s 
241183     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmodDivisible 
242197     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmodDivisible 
242262     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 59.96ms 
242265     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmodDivisibleRep.proof 
242265     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 88.5ns 
242266     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
245302     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.04s 
245302     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmodDivisibleRep 
246276     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmodDivisibleRep 
246280     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.77ms 
246282     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdivAddMultDenom.proof 
246282     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 66.5ns 
246283     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
249356     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.07s 
249356     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdivAddMultDenom 
250360     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdivAddMultDenom 
250596     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 221.19ms 
250599     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmodAltZero.proof 
250599     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 309.8ns 
250600     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
253698     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.1s 
253699     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmodAltZero 
254634     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmodAltZero 
254651     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 13.94ms 
254652     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmodAddMultDenomZero.proof 
254653     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 159.8ns 
254654     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
257768     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.11s 
257768     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmodAddMultDenomZero 
258788     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmodAddMultDenomZero 
258800     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 9.44ms 
258801     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_polyDiv_zero.proof 
258801     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 63.7ns 
258802     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
261904     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.1s 
261905     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: polyDiv_zero 
262903     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: polyDiv_zero 
262927     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 21.38ms 
262929     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_polyMod_ltdivDenom.proof 
262929     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 66ns 
262931     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
266039     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.11s 
266040     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: polyMod_ltdivDenom 
267049     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: polyMod_ltdivDenom 
267068     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 10.84ms 
267080     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_empty.proof 
267081     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 270.3ns 
267082     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
270091     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.01s 
270092     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_empty 
271074     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_empty 
271079     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.56ms 
271081     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_induction_upper.proof 
271081     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 83ns 
271082     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
274078     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3s 
274078     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_upper 
275081     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_induction_upper 
275088     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.15ms 
275092     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_induction_lower.proof 
275093     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 273.9ns 
275094     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
278059     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.97s 
278060     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_lower 
279052     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_induction_lower 
279091     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 35.25ms 
279092     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_bounds.proof 
279092     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 66ns 
279093     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
282278     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.18s 
282278     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_bounds 
283262     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_bounds 
283288     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 21.83ms 
283289     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_bounds2.proof 
283289     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 68.3ns 
283290     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
286394     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.1s 
286394     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_bounds2 
287348     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_bounds2 
287372     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 20.47ms 
287374     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_induction_upper2.proof 
287375     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 305.2ns 
287376     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
290446     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.07s 
290446     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_upper2 
291462     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_induction_upper2 
291466     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.62ms 
291468     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_induction_upper_concrete.proof 
291468     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 94.4ns 
291469     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
294576     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.11s 
294576     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_upper_concrete 
295554     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_induction_upper_concrete 
295560     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.01ms 
295561     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_induction_upper_concrete_2.proof 
295561     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 70.8ns 
295562     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
298703     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.14s 
298703     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_upper_concrete_2 
299726     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_induction_upper_concrete_2 
299737     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 7.64ms 
299739     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_induction_upper2_concrete.proof 
299739     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 73.5ns 
299740     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
302914     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.17s 
302914     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_upper2_concrete 
303945     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_induction_upper2_concrete 
303949     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.18ms 
303951     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_induction_lower_concrete.proof 
303951     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 101.1ns 
303952     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
307067     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.12s 
307067     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_lower_concrete 
308087     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_induction_lower_concrete 
308090     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 987.49ns 
308092     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_induction_lower2.proof 
308092     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 76.2ns 
308093     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
311238     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.15s 
311238     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_lower2 
312270     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_induction_lower2 
312275     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.66ms 
312277     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_induction_lower2_concrete.proof 
312277     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 81.7ns 
312278     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
315385     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.11s 
315385     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_lower2_concrete 
316385     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_induction_lower2_concrete 
316389     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.72ms 
316392     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_positive.proof 
316392     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 328.8ns 
316393     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
319522     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.13s 
319522     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_positive 
320532     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_positive 
320609     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 68.35ms 
320611     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_upper_bound.proof 
320612     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 242.5ns 
320613     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
323780     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.17s 
323780     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_upper_bound 
324793     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_upper_bound 
324852     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 54.46ms 
324854     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_lower_bound.proof 
324854     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 124.1ns 
324854     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
327997     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.14s 
327998     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_lower_bound 
329019     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_lower_bound 
329070     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 46.88ms 
329073     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_positive_lower_bound_element.proof 
329073     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 81.1ns 
329074     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
332178     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.1s 
332178     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_positive_lower_bound_element 
333182     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_positive_lower_bound_element 
333270     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 79.04ms 
333276     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_sub_same_index.proof 
333276     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 259.5ns 
333277     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
336481     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.2s 
336482     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_sub_same_index 
337507     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_sub_same_index 
337564     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 53.11ms 
337566     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_less_same_index.proof 
337566     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 95.4ns 
337567     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
340800     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.23s 
340800     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_less_same_index 
341845     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_less_same_index 
341937     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 85.5ms 
341939     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_equal_except_one_index.proof 
341939     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 235.2ns 
341940     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
345133     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.19s 
345134     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_equal_except_one_index 
346174     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_equal_except_one_index 
346220     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 41.9ms 
346222     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_is_max.proof 
346222     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 83.4ns 
346223     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
349434     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.21s 
349434     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_is_max 
350463     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_is_max 
350496     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 29.1ms 
350498     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_is_max2.proof 
350498     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 90.3ns 
350499     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
353748     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.25s 
353748     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_is_max2 
354769     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_is_max2 
354846     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 73.45ms 
354850     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_is_max3.proof 
354850     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 197ns 
354851     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
358058     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.21s 
358058     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_is_max3 
359096     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_is_max3 
359132     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 32.05ms 
359134     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_is_max4.proof 
359134     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 84.8ns 
359135     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
362397     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.26s 
362397     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_is_max4 
363459     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_is_max4 
363508     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 44.75ms 
363510     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_lt_max.proof 
363510     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 81ns 
363511     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
366698     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.19s 
366698     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_lt_max 
367743     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_lt_max 
367788     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 40.61ms 
367789     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_lt_max2.proof 
367790     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 89.5ns 
367790     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
370968     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.18s 
370969     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_lt_max2 
372008     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_lt_max2 
372050     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 38.02ms 
372052     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_lt_max3.proof 
372052     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 85.8ns 
372053     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
375232     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.18s 
375232     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_lt_max3 
376249     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_lt_max3 
376298     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 44.34ms 
376300     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_lt_max4.proof 
376300     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 126.7ns 
376302     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
379418     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.12s 
379418     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_lt_max4 
380368     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_lt_max4 
380405     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 33.61ms 
380407     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_gt0.proof 
380407     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 73.1ns 
380408     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
383485     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.08s 
383485     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_gt0 
384504     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_gt0 
384547     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 40.15ms 
384549     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_gt0_alt.proof 
384549     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 84.4ns 
384550     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
387756     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.21s 
387756     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_gt0_alt 
388771     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_gt0_alt 
388815     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 39.78ms 
388817     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_add_concrete.proof 
388817     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 79ns 
388818     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
391971     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.15s 
391971     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_add_concrete 
392976     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_add_concrete 
392987     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 8.66ms 
392988     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bprod/Taclet_bprod_all_positive.proof 
392988     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 72ns 
392989     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
396062     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.07s 
396062     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bprod_all_positive 
397097     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bprod_all_positive 
397124     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 24.36ms 
397126     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bprod/Taclet_bprod_split.proof 
397126     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 63.4ns 
397127     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
400363     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.24s 
400363     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bprod_split 
401422     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bprod_split 
401428     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.04ms 
401430     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powConcrete0.proof 
401430     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 89.3ns 
401431     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
404616     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.18s 
404616     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powConcrete0 
405634     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powConcrete0 
405637     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 921.5ns 
405639     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powConcrete1.proof 
405639     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 70.6ns 
405640     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
408752     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.11s 
408753     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powConcrete1 
409789     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powConcrete1 
409792     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.22ms 
409795     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powSplitFactor.proof 
409796     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 548.9ns 
409797     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
413040     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.24s 
413040     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powSplitFactor 
414052     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powSplitFactor 
414062     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 7.44ms 
414064     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powAdd.proof 
414064     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 88.6ns 
414065     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
417177     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.11s 
417177     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powAdd 
418169     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powAdd 
418179     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 7.01ms 
418180     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powMono.proof 
418180     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 67.5ns 
418181     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
421406     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.22s 
421406     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powMono 
422462     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powMono 
422483     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 17.44ms 
422484     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powMonoConcrete.proof 
422485     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 78.1ns 
422485     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
425595     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.11s 
425596     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powMonoConcrete 
426625     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powMonoConcrete 
426630     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.81ms 
426632     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powMonoConcreteRight.proof 
426632     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 67.2ns 
426633     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
429742     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.11s 
429742     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powMonoConcreteRight 
430774     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powMonoConcreteRight 
430777     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 735.9ns 
430779     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powPositive.proof 
430779     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 91.1ns 
430780     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
433910     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.13s 
433910     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powPositive 
434952     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powPositive 
434960     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 5.5ms 
434961     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powPositiveConcrete.proof 
434961     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 70.3ns 
434962     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
438133     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.17s 
438133     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powPositiveConcrete 
439164     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powPositiveConcrete 
439167     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.07ms 
439168     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powGeq1Concrete.proof 
439169     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 87.9ns 
439169     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
442356     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.19s 
442356     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powGeq1Concrete 
443429     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powGeq1Concrete 
443432     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 889.5ns 
443434     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_pow2InIntLower.proof 
443434     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 182.5ns 
443435     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
446724     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.29s 
446724     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: pow2InIntLower 
447745     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: pow2InIntLower 
447748     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.03ms 
447750     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_pow2InIntUpper.proof 
447750     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 237.6ns 
447751     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
450984     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.23s 
450984     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: pow2InIntUpper 
451982     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: pow2InIntUpper 
451987     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.91ms 
451989     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logSelfConcrete.proof 
451989     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 80.6ns 
451990     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
455220     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.23s 
455220     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logSelfConcrete 
456266     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logSelfConcrete 
456281     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 11.78ms 
456282     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_log1Concrete.proof 
456283     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 81.2ns 
456283     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
459425     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.14s 
459425     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: log1Concrete 
460457     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: log1Concrete 
460462     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.37ms 
460464     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logProduct.proof 
460464     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 75.4ns 
460465     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
463655     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.19s 
463655     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logProduct 
464685     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logProduct 
464696     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 7.56ms 
464697     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logTimesBaseConcrete.proof 
464697     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 62.6ns 
464698     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
467834     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.14s 
467834     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logTimesBaseConcrete 
468890     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logTimesBaseConcrete 
468899     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 5.18ms 
468901     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logProdIdentity.proof 
468901     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 167.9ns 
468902     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
472056     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.15s 
472056     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logProdIdentity 
473091     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logProdIdentity 
473116     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 21.3ms 
473118     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logProdIdentityConcrete.proof 
473118     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 87ns 
473119     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
476276     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.16s 
476276     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logProdIdentityConcrete 
477307     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logProdIdentityConcrete 
477312     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.79ms 
477313     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logPowIdentity.proof 
477313     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 70.8ns 
477314     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
480562     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.25s 
480562     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logPowIdentity 
481569     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logPowIdentity 
481574     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.14ms 
481576     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logPowIdentityConcrete.proof 
481576     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 56.9ns 
481576     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
484843     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.27s 
484843     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logPowIdentityConcrete 
485860     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logPowIdentityConcrete 
485865     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.8ms 
485866     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logPositive.proof 
485866     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 73.3ns 
485867     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
489132     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.26s 
489132     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logPositive 
490193     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logPositive 
490218     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 22.28ms 
490220     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logPositiveConcrete.proof 
490220     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 71ns 
490221     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
493416     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.2s 
493416     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logPositiveConcrete 
494486     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logPositiveConcrete 
494492     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 703.1ns 
494494     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logMono.proof 
494494     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 75.3ns 
494496     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
497712     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.22s 
497712     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logMono 
498762     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logMono 
498821     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 53.83ms 
498823     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logMonoConcrete.proof 
498823     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 79.6ns 
498824     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
502081     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.26s 
502081     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logMonoConcrete 
503172     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logMonoConcrete 
503178     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.73ms 
503180     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powLogLess.proof 
503181     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 325.5ns 
503182     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
506393     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.21s 
506393     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powLogLess 
507434     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powLogLess 
507469     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 31.63ms 
507471     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powLogMore2.proof 
507471     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 69.6ns 
507472     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
510652     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.18s 
510653     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powLogMore2 
511633     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powLogMore2 
511671     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 34.43ms 
511675     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logLessThanPow.proof 
511676     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 289.7ns 
511677     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
514911     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.23s 
514911     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logLessThanPow 
515932     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logLessThanPow 
515969     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 33.17ms 
515971     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logLessThanPowConcrete.proof 
515971     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 118.8ns 
515972     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
519227     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.26s 
519227     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logLessThanPowConcrete 
520266     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logLessThanPowConcrete 
520269     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 810.4ns 
520271     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logSqueeze.proof 
520271     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 75.9ns 
520272     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
523530     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.26s 
523530     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logSqueeze 
524555     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logSqueeze 
524562     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 5.63ms 
524564     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/booleanRules/Taclet_ifthenelse_equals.proof 
524564     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 87.4ns 
524565     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
527727     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.16s 
527727     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: ifthenelse_equals 
528786     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: ifthenelse_equals 
528790     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.16ms 
528791     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/booleanRules/Taclet_ifthenelse_equals_1.proof 
528792     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 180ns 
528792     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
532023     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.23s 
532023     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: ifthenelse_equals_1 
533060     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: ifthenelse_equals_1 
533064     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.11ms 
533065     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/booleanRules/Taclet_ifthenelse_equals_2.proof 
533066     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 70.4ns 
533066     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
536278     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.21s 
536278     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: ifthenelse_equals_2 
537319     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: ifthenelse_equals_2 
537323     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.15ms 
537324     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/locSet/Taclet_disjointWithSingleton1.proof 
537324     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 59ns 
537325     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
540539     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.21s 
540539     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: disjointWithSingleton1 
541573     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: disjointWithSingleton1 
541578     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.93ms 
541579     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/locSet/Taclet_disjointWithSingleton2.proof 
541579     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 71.6ns 
541580     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
544823     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.24s 
544823     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: disjointWithSingleton2 
545889     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: disjointWithSingleton2 
545893     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.69ms 
545894     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/locSet/Taclet_disjointArrayRanges.proof 
545894     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 64.7ns 
545895     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
549068     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.17s 
549068     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: disjointArrayRanges 
550133     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: disjointArrayRanges 
550147     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 11.14ms 
550149     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/locSet/Taclet_disjointArrayRangeAllFields1.proof 
550149     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 62.7ns 
550150     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
553323     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.17s 
553323     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: disjointArrayRangeAllFields1 
554373     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: disjointArrayRangeAllFields1 
554395     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 19.67ms 
554403     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/locSet/Taclet_disjointArrayRangeAllFields2.proof 
554404     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 557.2ns 
554405     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
557577     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.17s 
557577     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: disjointArrayRangeAllFields2 
558632     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: disjointArrayRangeAllFields2 
558648     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 13.08ms 
558649     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqSelfDefinition.proof 
558649     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 92.7ns 
558650     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
561798     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.15s 
561799     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqSelfDefinition 
562812     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqSelfDefinition 
562828     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 13.89ms 
562830     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqOutsideValue.proof 
562830     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 70.2ns 
562831     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
565940     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.11s 
565940     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqOutsideValue 
566960     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqOutsideValue 
566966     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.12ms 
566968     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_castedGetAny.proof 
566968     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 74ns 
566969     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
569981     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.01s 
569981     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: castedGetAny 
570995     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: castedGetAny 
571002     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 5.97ms 
571004     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqGetAlphaCast.proof 
571004     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 66.2ns 
571005     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
574012     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.01s 
574012     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqGetAlphaCast 
575022     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqGetAlphaCast 
575025     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 925.6ns 
575026     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqSingleton.proof 
575026     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 62ns 
575027     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
578086     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.06s 
578086     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqSingleton 
579056     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqSingleton 
579060     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.71ms 
579061     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqSingletonConcrete.proof 
579061     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 79.1ns 
579062     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
582092     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.03s 
582093     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqSingletonConcrete 
583123     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqSingletonConcrete 
583126     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.19ms 
583128     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqConcat.proof 
583128     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 68ns 
583129     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
586130     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3s 
586130     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqConcat 
587154     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqConcat 
587171     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 13.81ms 
587172     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqSub.proof 
587172     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 63.1ns 
587173     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
590257     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.08s 
590257     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqSub 
591239     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqSub 
591245     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.19ms 
591247     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqReverse.proof 
591247     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 70ns 
591248     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
594321     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.07s 
594321     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqReverse 
595342     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqReverse 
595351     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 7.16ms 
595353     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqEmpty.proof 
595353     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 112.4ns 
595354     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
598360     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.01s 
598360     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqEmpty 
599375     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqEmpty 
599378     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 881.1ns 
599379     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqSingleton.proof 
599379     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 83.2ns 
599380     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
602334     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.95s 
602334     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqSingleton 
603322     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqSingleton 
603325     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 975.3ns 
603326     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqConcat.proof 
603327     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 68.1ns 
603331     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
606425     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.09s 
606425     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqConcat 
607455     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqConcat 
607460     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.22ms 
607462     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqSub.proof 
607463     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 115.9ns 
607463     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
610495     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.03s 
610495     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqSub 
611513     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqSub 
611518     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.02ms 
611520     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqReverse.proof 
611520     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 97.1ns 
611520     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
614534     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.01s 
614535     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqReverse 
615529     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqReverse 
615533     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.23ms 
615535     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_equalityToSeqGetAndSeqLenLeft.proof 
615535     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 56.1ns 
615535     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
618582     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.05s 
618583     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: equalityToSeqGetAndSeqLenLeft 
619589     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: equalityToSeqGetAndSeqLenLeft 
619593     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.89ms 
619594     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_equalityToSeqGetAndSeqLenRight.proof 
619594     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 82.1ns 
619595     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
622641     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.05s 
622642     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: equalityToSeqGetAndSeqLenRight 
623646     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: equalityToSeqGetAndSeqLenRight 
623653     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 5.01ms 
623655     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqSingletonEQ.proof 
623655     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 65.7ns 
623656     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
626694     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.04s 
626694     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqSingletonEQ 
627655     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqSingletonEQ 
627659     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.86ms 
627660     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqConcatEQ.proof 
627661     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 83.5ns 
627661     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
630707     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.05s 
630708     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqConcatEQ 
631704     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqConcatEQ 
631720     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 13.45ms 
631721     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqSubEQ.proof 
631722     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 122.3ns 
631722     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
634696     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.97s 
634697     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqSubEQ 
635708     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqSubEQ 
635711     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 873.1ns 
635712     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqReverseEQ.proof 
635712     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 80.5ns 
635713     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
638785     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.07s 
638785     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqReverseEQ 
639786     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqReverseEQ 
639796     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 8.4ms 
639798     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqEmptyEQ.proof 
639798     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 89.3ns 
639799     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
642882     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.08s 
642882     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqEmptyEQ 
643907     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqEmptyEQ 
643910     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.28ms 
643911     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqSingletonEQ.proof 
643912     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 64.6ns 
643912     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
646983     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.07s 
646983     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqSingletonEQ 
647990     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqSingletonEQ 
647993     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.15ms 
647995     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqConcatEQ.proof 
647995     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 65.4ns 
647996     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
651027     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.03s 
651028     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqConcatEQ 
652054     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqConcatEQ 
652061     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.68ms 
652062     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqSubEQ.proof 
652062     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 54.2ns 
652063     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
655090     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.03s 
655091     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqSubEQ 
656110     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqSubEQ 
656114     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.27ms 
656115     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqReverseEQ.proof 
656115     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 55.9ns 
656116     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
659129     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.01s 
659130     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqReverseEQ 
660160     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqReverseEQ 
660165     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.93ms 
660167     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqDefEQ.proof 
660167     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 94.8ns 
660167     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
663234     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.07s 
663234     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqDefEQ 
664238     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqDefEQ 
664243     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.27ms 
664244     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqDefEQ.proof 
664244     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 49.2ns 
664245     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
667341     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.1s 
667341     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqDefEQ 
668381     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqDefEQ 
668388     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.95ms 
668389     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqConcatWithSeqEmpty1.proof 
668389     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 49.6ns 
668390     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
671538     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.15s 
671539     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqConcatWithSeqEmpty1 
672594     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqConcatWithSeqEmpty1 
672615     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 18.95ms 
672617     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqConcatWithSeqEmpty2.proof 
672617     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 89.3ns 
672618     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
675737     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.12s 
675737     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqConcatWithSeqEmpty2 
676771     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqConcatWithSeqEmpty2 
676794     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 19.88ms 
676795     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqReverseOfSeqEmpty.proof 
676795     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 68.2ns 
676796     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
679878     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.08s 
679878     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqReverseOfSeqEmpty 
680932     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqReverseOfSeqEmpty 
680945     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 11.68ms 
680947     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_subSeqComplete.proof 
680947     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 78.1ns 
680948     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
683953     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.01s 
683954     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: subSeqComplete 
684957     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: subSeqComplete 
684972     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 12.67ms 
684973     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_subSeqTailR.proof 
684973     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 100.6ns 
684974     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
687995     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.02s 
687996     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: subSeqTailR 
688974     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: subSeqTailR 
689009     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 32.66ms 
689011     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_subSeqTailL.proof 
689011     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 67.1ns 
689012     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
692048     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.04s 
692048     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: subSeqTailL 
693080     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: subSeqTailL 
693120     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 36.54ms 
693122     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_subSeqTailEQR.proof 
693122     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 87.2ns 
693123     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
696148     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.02s 
696148     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: subSeqTailEQR 
697195     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: subSeqTailEQR 
697266     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 67.92ms 
697269     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_subSeqTailEQL.proof 
697269     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 77.8ns 
697269     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
700327     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.06s 
700327     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: subSeqTailEQL 
701359     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: subSeqTailEQL 
701381     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 19.31ms 
701383     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDef_split.proof 
701383     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 70ns 
701384     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
704449     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.07s 
704449     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_split 
705468     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDef_split 
705518     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 46.28ms 
705519     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDef_induction_upper.proof 
705519     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 60.8ns 
705520     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
708472     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.95s 
708472     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_induction_upper 
709470     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDef_induction_upper 
709544     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 70.29ms 
709546     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDef_induction_upper_concrete.proof 
709546     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 73ns 
709547     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
712694     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.15s 
712694     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_induction_upper_concrete 
713737     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDef_induction_upper_concrete 
713808     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 67.22ms 
713811     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDef_induction_lower.proof 
713811     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 209ns 
713812     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
716873     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.06s 
716873     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_induction_lower 
717878     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDef_induction_lower 
717938     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 55.79ms 
717940     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDef_induction_lower_concrete.proof 
717940     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 62.5ns 
717941     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
720945     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3s 
720945     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_induction_lower_concrete 
721939     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDef_induction_lower_concrete 
722004     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 61.03ms 
722006     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDef_split_in_three.proof 
722006     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 55.9ns 
722007     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
724916     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.91s 
724916     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_split_in_three 
725912     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDef_split_in_three 
726075     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 152.69ms 
726077     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDef_empty.proof 
726077     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 66ns 
726078     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
729067     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.99s 
729068     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_empty 
730038     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDef_empty 
730049     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 9.11ms 
730051     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDef_one_summand.proof 
730051     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 91.3ns 
730051     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
732967     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.92s 
732967     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_one_summand 
733939     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDef_one_summand 
733950     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 9.19ms 
733951     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDef_lower_equals_upper.proof 
733951     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 63.1ns 
733952     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
736971     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.02s 
736971     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_lower_equals_upper 
737936     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDef_lower_equals_upper 
737943     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.77ms 
737944     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDefOfSeq.proof 
737944     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 70.3ns 
737945     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
740936     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.99s 
740937     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDefOfSeq 
741931     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDefOfSeq 
741960     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 24.03ms 
741962     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqSelfDefinitionEQ2.proof 
741963     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 454.5ns 
741964     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
744996     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.03s 
744997     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqSelfDefinitionEQ2 
745992     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqSelfDefinitionEQ2 
746007     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 13.1ms 
746009     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_indexOfSeqSingleton.proof 
746009     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 83.3ns 
746010     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
749074     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.06s 
749074     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: indexOfSeqSingleton 
750108     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: indexOfSeqSingleton 
750113     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.79ms 
750115     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_indexOfSeqConcatFirst.proof 
750115     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 76.3ns 
750116     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
753172     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.06s 
753172     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: indexOfSeqConcatFirst 
754192     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: indexOfSeqConcatFirst 
754217     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 22.22ms 
754219     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_indexOfSeqConcatSecond.proof 
754219     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 86.8ns 
754220     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
757286     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.07s 
757286     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: indexOfSeqConcatSecond 
758307     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: indexOfSeqConcatSecond 
758337     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 27.29ms 
758339     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_indexOfSeqSub.proof 
758339     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 75.1ns 
758340     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
761371     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.03s 
761371     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: indexOfSeqSub 
762367     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: indexOfSeqSub 
762399     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 28.02ms 
762400     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfArray2seq.proof 
762400     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 58.5ns 
762401     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
765452     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.05s 
765452     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfArray2seq 
766465     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfArray2seq 
766470     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.07ms 
766472     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getAnyOfArray2seq.proof 
766472     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 67ns 
766473     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
769533     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.06s 
769533     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getAnyOfArray2seq 
770532     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getAnyOfArray2seq 
770537     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.06ms 
770538     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfArray2seq.proof 
770538     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 61.6ns 
770539     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
773734     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.2s 
773734     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfArray2seq 
774768     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfArray2seq 
774776     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 6.45ms 
774778     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_getAnyOfNPermInv.proof 
774778     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 82.6ns 
774779     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
777908     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.13s 
777908     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getAnyOfNPermInv 
778947     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getAnyOfNPermInv 
778955     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 6.64ms 
778957     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqNPermRange.proof 
778957     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 57.3ns 
778958     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
782035     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.08s 
782035     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqNPermRange 
783063     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqNPermRange 
783181     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 111.63ms 
783182     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermTrans.proof 
783182     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 93ns 
783183     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
786266     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.08s 
786266     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermTrans 
787296     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermTrans 
787338     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 38.4ms 
787340     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermRefl.proof 
787340     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 202.41ns 
787341     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
790458     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.12s 
790458     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermRefl 
791483     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermRefl 
791517     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 30.95ms 
791518     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermSplit.proof 
791519     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 73.8ns 
791519     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
794655     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.14s 
794655     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermSplit 
795677     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermSplit 
795680     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 541.41ns 
795681     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqNPermRight.proof 
795681     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 53ns 
795682     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
798696     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.01s 
798697     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqNPermRight 
799711     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqNPermRight 
800007     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 284.43ms 
800009     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermFromSwap.proof 
800009     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 63.6ns 
800010     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
803073     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.06s 
803073     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermFromSwap 
804088     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermFromSwap 
804167     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 73.71ms 
804169     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermTransAlt0.proof 
804169     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 56.3ns 
804169     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
807157     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.99s 
807157     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermTransAlt0 
808199     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermTransAlt0 
808201     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 443.4ns 
808203     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermTransAlt1.proof 
808203     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 58.7ns 
808204     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
811253     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.05s 
811253     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermTransAlt1 
812287     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermTransAlt1 
812289     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 532.21ns 
812291     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermTransAlt2.proof 
812291     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 84.3ns 
812292     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
815411     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.12s 
815412     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermTransAlt2 
816507     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermTransAlt2 
816510     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 538.9ns 
816511     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermTransAlt3.proof 
816511     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 78.9ns 
816512     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
819584     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.07s 
819584     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermTransAlt3 
820601     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermTransAlt3 
820604     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 685.8ns 
820605     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermForall.proof 
820605     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 69.3ns 
820606     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
823655     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.05s 
823655     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermForall 
824679     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermForall 
824770     INFO  Test worker     d.u.i.k.s.SMTFocusResults Analyzing unsat core: (L_1 L_3 L_4) 
824790     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 108.43ms 
824793     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermExists.proof 
824793     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 224.7ns 
824794     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
827822     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.03s 
827822     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermExists 
828892     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermExists 
828956     INFO  Test worker     d.u.i.k.s.SMTFocusResults Analyzing unsat core: (L_1 L_3 L_5 L_6 L_7) 
828957     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 61.58ms 
828958     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm2/Taclet_schiffl_lemma_2.proof 
828958     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 67ns 
828960     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
832195     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.23s 
832195     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: schiffl_lemma_2 
833264     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: schiffl_lemma_2 
833266     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.2ns 
833306     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 1: 'macro split-prop' 
833364     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 2: 'rule allRight' 
833401     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 3: 'rule allRight' 
833411     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 4: 'macro split-prop' 
833424     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 5: 'rule 'seqPermDefLeft'' 
833428     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 6: 'rule 'andLeft'' 
833429     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 7: 'rule 'exLeft'' 
833433     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 8: 'macro split-prop' 
833438     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 9: 'rule  seqNPermRange' 
833440     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 10: 'instantiate var=iv with='v_x_0' occ=1' 
833446     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 11: 'rule impLeft' 
833449     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 12: 'tryclose branch' 
833782     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 13: 'rule andLeft' 
833784     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 14: 'rule andLeft' 
833785     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 15: 'instantiate var=iv with='v_y_0' occ=1' 
833787     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 16: 'rule impLeft' 
833788     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 17: 'tryclose branch' 
833997     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 18: 'rule andLeft' 
833999     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 19: 'rule andLeft' 
834002     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 20: 'rule seqNPermDefLeft' 
834005     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 21: 'instantiate var=iv with='v_x_0' occ=2' 
834006     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 22: 'rule impLeft' 
834007     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 23: 'tryclose branch' 
834234     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 24: 'rule exLeft' 
834237     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 25: 'rule andLeft' 
834238     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 26: 'rule andLeft' 
834239     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 27: 'instantiate hide var=iv with='v_y_0' occ=2' 
834241     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 28: 'rule impLeft' 
834244     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 29: 'tryclose branch' 
834393     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 30: 'rule exLeft' 
834395     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 31: 'rule andLeft' 
834397     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 32: 'rule andLeft' 
834398     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 33: 'instantiate var=iv with='jv_0' occ=1' 
834399     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 34: 'rule impLeft' 
834400     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 35: 'tryclose branch' 
834416     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 36: 'rule andLeft' 
834417     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 37: 'rule andLeft' 
834418     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 38: 'rule castAdd formula='s_0[jv_0] = v_x_0' occ=0' 
834420     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 39: 'instantiate hide var=iv with='jv_1' occ=1' 
834423     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 40: 'rule impLeft' 
834424     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 41: 'tryclose branch' 
834437     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 42: 'rule andLeft' 
834438     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 43: 'rule andLeft' 
834439     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 44: 'rule castAdd formula='s_0[jv_1] = v_y_0' occ=0' 
834441     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 45: 'instantiate var=iv  with='v_x_0'' 
834442     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 46: 'rule impLeft' 
834443     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 47: 'tryclose branch' 
834645     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 48: 'instantiate var=iv  with='v_y_0'' 
834646     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 49: 'rule impLeft' 
834651     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 50: 'tryclose branch' 
834840     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 51: 'cut 'v_x_0 = v_y_0'' 
834842     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)'' 
834846     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 53: 'rule andRight' 
834847     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 54: 'rule andRight' 
834848     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 55: 'rule andRight' 
834850     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 56: 'rule andRight' 
834851     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 57: 'rule lenOfSwap' 
834854     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 58: 'tryclose branch' 
834860     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 59: 'rule seqNPermSwapNPerm' 
834861     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 60: 'instantiate hide var='iv' with='v_x_0' occ=1' 
834863     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 61: 'instantiate hide var='jv' with='jv_0'' 
834864     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 62: 'rule impLeft' 
834865     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 63: 'tryclose branch' 
835037     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 64: 'tryclose branch' 
835042     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 65: 'rule allRight' 
835045     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 66: 'rule impRight' 
835045     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 67: 'rule andLeft' 
835046     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 68: 'instantiate var=iv with='v_iv_0'' 
835048     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 69: 'rule impLeft' 
835050     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 70: 'tryclose branch' 
835241     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 71: 'rule getOfSwap' 
835243     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 72: 'rule ifthenelse_negated' 
835244     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 73: 'rule ifthenelse_split occ=0' 
835246     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 74: 'rule andLeft' 
835247     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 75: 'rule andLeft' 
835248     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 76: 'rule andLeft' 
835249     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 77: 'rule ifthenelse_split occ=0' 
835251     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 78: 'tryclose branch' 
835378     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 79: 'rule ifthenelse_split occ=0' 
835380     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 80: 'tryclose branch' 
835501     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 81: 'tryclose branch' 
835505     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 82: 'tryclose branch' 
835512     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 83: 'rule getOfSwap' 
835514     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 84: 'rule ifthenelse_negated' 
835517     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 85: 'rule ifthenelse_split occ=0' 
835519     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 86: 'rule andLeft' 
835520     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 87: 'rule andLeft' 
835520     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 88: 'rule andLeft' 
835521     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 89: 'rule ifthenelse_split occ=0' 
835522     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 90: 'tryclose branch' 
835533     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 91: 'tryclose branch' 
835538     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 92: 'tryclose branch' 
835668     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 93: 'rule getOfSwap' 
835670     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 94: 'rule ifthenelse_negated' 
835673     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 95: 'rule ifthenelse_split occ=0' 
835675     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 96: 'rule andLeft' 
835675     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 97: 'rule andLeft' 
835676     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 98: 'rule andLeft' 
835677     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 99: 'rule ifthenelse_split occ=0' 
835678     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 100: 'tryclose branch' 
835753     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 101: 'tryclose branch' 
835761     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 102: 'tryclose branch' 
835889     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 103: 'cut '(int)s_0[v_x_0] = (int)s_0[v_y_0]'' 
835891     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 104: 'rule seqNPermInjective' 
835894     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 105: 'instantiate hide var=iv with='v_x_0'' 
835895     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 106: 'instantiate hide var=jv with='v_y_0'' 
835896     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 107: 'rule impLeft' 
835900     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 108: 'tryclose branch' 
836075     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 109: 'tryclose branch' 
836080     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 110: 'cut '(int)s_0[v_x_0] = v_x_0'' 
836084     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)'' 
836087     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 112: 'rule andRight' 
836089     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 113: 'rule andRight' 
836090     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 114: 'rule andRight' 
836091     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 115: 'rule andRight' 
836092     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 116: 'tryclose branch' 
836104     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 117: 'rule seqNPermSwapNPerm' 
836111     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 118: 'instantiate hide var=iv with='v_y_0'' 
836113     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 119: 'instantiate hide var=jv with='jv_1'' 
836114     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 120: 'tryclose branch' 
836243     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 121: 'rule allRight' 
836246     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 122: 'rule impRight' 
836247     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 123: 'rule andLeft' 
836249     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 124: 'instantiate var=iv with='v_iv_0'' 
836251     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 125: 'rule impLeft' 
836252     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 126: 'tryclose branch' 
836398     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 127: 'rule getOfSwap' 
836400     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 128: 'rule ifthenelse_negated' 
836401     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 129: 'rule ifthenelse_split occ=0' 
836403     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 130: 'rule andLeft' 
836404     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 131: 'rule andLeft' 
836405     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 132: 'rule andLeft' 
836406     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 133: 'rule ifthenelse_split occ=0' 
836408     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 134: 'tryclose branch' 
836520     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 135: 'rule ifthenelse_split occ=0' 
836523     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 136: 'tryclose branch' 
836639     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 137: 'instantiate var=iv with='v_y_0'' 
836639     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 138: 'rule impLeft' 
836641     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 139: 'tryclose branch' 
836646     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 140: 'tryclose branch' 
836651     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 141: 'tryclose branch' 
836657     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 142: 'tryclose branch' 
836831     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 143: 'rule getOfSwap' 
836833     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 144: 'rule ifthenelse_negated' 
836834     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 145: 'rule ifthenelse_split occ=0' 
836835     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 146: 'tryclose branch' 
836879     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 147: 'tryclose branch' 
836995     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 148: 'tryclose branch' 
841571     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 149: 'cut  '(int)s_0[v_y_0] = v_y_0'' 
841573     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)'' 
841579     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 151: 'rule andRight' 
841580     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 152: 'rule andRight' 
841581     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 153: 'rule andRight' 
841582     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 154: 'rule andRight' 
841584     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 155: 'tryclose branch' 
841594     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 156: 'rule seqNPermSwapNPerm' 
841596     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 157: 'instantiate hide var=iv with='v_x_0'' 
841597     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 158: 'instantiate hide var=jv with='jv_0'' 
841598     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 159: 'rule impLeft' 
841599     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 160: 'tryclose branch' 
841720     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 161: 'tryclose branch' 
841725     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 162: 'rule allRight' 
841727     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 163: 'rule impRight' 
841727     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 164: 'rule andLeft' 
841728     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 165: 'instantiate var=iv with='v_iv_0'' 
841729     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 166: 'rule impLeft' 
841730     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 167: 'tryclose branch' 
841861     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 168: 'rule getOfSwap' 
841863     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 169: 'rule ifthenelse_negated' 
841865     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 170: 'rule ifthenelse_split occ=0' 
841866     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 171: 'rule andLeft' 
841867     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 172: 'rule andLeft' 
841868     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 173: 'rule andLeft' 
841869     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 174: 'rule ifthenelse_split occ=0' 
841870     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 175: 'tryclose branch' 
841968     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 176: 'rule ifthenelse_split occ=0' 
841970     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 177: 'tryclose branch' 
842068     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 178: 'tryclose branch' 
842073     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 179: 'tryclose branch' 
842079     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 180: 'rule getOfSwap' 
842080     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 181: 'rule ifthenelse_negated' 
842081     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 182: 'rule ifthenelse_split occ=0' 
842083     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 183: 'tryclose branch' 
842099     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 184: 'tryclose branch' 
842202     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 185: 'rule getOfSwap' 
842204     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 186: 'rule ifthenelse_negated' 
842204     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 187: 'rule ifthenelse_split occ=0' 
842205     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 188: 'tryclose branch' 
842301     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 189: 'tryclose branch' 
842312     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 190: 'cut '(int)s_0[v_x_0]=v_y_0'' 
842313     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)'' 
842316     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 192: 'rule andRight' 
842317     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 193: 'rule andRight' 
842317     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 194: 'rule andRight' 
842318     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 195: 'rule andRight' 
842319     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 196: 'tryclose branch' 
842333     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 197: 'rule seqNPermSwapNPerm' 
842334     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 198: 'instantiate hide var=iv with='jv_0'' 
842335     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 199: 'instantiate hide var=jv with='v_x_0'' 
842336     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 200: 'rule impLeft' 
842343     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 201: 'tryclose branch' 
842462     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 202: 'rule seqNPermSwapNPerm formula='seqNPerm(seqSwap(s_0, jv_0, v_x_0))'' 
842464     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 203: 'instantiate hide var=iv with='jv_0'' 
842466     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 204: 'instantiate hide var=jv with='v_y_0'' 
842468     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 205: 'rule impLeft' 
842469     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 206: 'tryclose branch' 
842594     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 207: 'tryclose branch' 
842601     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 208: 'rule allRight' 
842603     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 209: 'rule impRight' 
842604     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 210: 'rule andLeft' 
842605     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 211: 'instantiate var=iv with='v_iv_0'' 
842606     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 212: 'rule impLeft' 
842607     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 213: 'tryclose branch' 
842795     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 214: 'rule getOfSwap' 
842798     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 215: 'rule ifthenelse_negated' 
842799     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 216: 'rule ifthenelse_split occ=0' 
842801     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 217: 'rule andLeft' 
842803     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 218: 'rule andLeft' 
842805     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 219: 'rule andLeft' 
842806     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 220: 'rule ifthenelse_split occ=0' 
842808     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 221: 'rule getOfSwap' 
842809     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 222: 'rule ifthenelse_negated' 
842810     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 223: 'rule ifthenelse_split occ=0' 
842812     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 224: 'rule andLeft' 
842812     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 225: 'rule andLeft' 
842813     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 226: 'rule andLeft' 
842814     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 227: 'rule ifthenelse_split occ=0' 
842815     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 228: 'tryclose branch' 
842931     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 229: 'rule ifthenelse_split occ=0' 
842933     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 230: 'tryclose branch' 
842941     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 231: 'tryclose branch' 
843035     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 232: 'tryclose branch' 
843136     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 233: 'rule ifthenelse_split' 
843138     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 234: 'rule getOfSwap' 
843139     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 235: 'rule ifthenelse_negated' 
843140     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 236: 'rule ifthenelse_split occ=0' 
843141     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 237: 'rule andLeft' 
843141     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 238: 'rule andLeft' 
843142     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 239: 'rule andLeft' 
843142     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 240: 'rule ifthenelse_split occ=0' 
843143     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 241: 'tryclose branch' 
843254     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 242: 'tryclose branch' 
843261     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 243: 'tryclose branch' 
843377     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 244: 'rule getOfSwap' 
843378     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 245: 'rule ifthenelse_negated' 
843379     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 246: 'rule ifthenelse_split occ=0' 
843380     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 247: 'rule andLeft' 
843380     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 248: 'rule andLeft' 
843381     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 249: 'rule andLeft' 
843381     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 250: 'rule ifthenelse_split occ=0' 
843382     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 251: 'tryclose branch' 
843388     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 252: 'rule ifthenelse_split occ=0' 
843389     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 253: 'tryclose branch' 
843489     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 254: 'tryclose branch' 
843496     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 255: 'tryclose branch' 
843502     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 256: 'tryclose branch' 
843628     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 257: 'rule getOfSwap' 
843630     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 258: 'rule ifthenelse_negated' 
843631     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 259: 'rule ifthenelse_split occ=0' 
843632     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 260: 'rule andLeft' 
843632     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 261: 'rule andLeft' 
843633     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 262: 'rule andLeft' 
843633     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 263: 'rule ifthenelse_split occ=0' 
843634     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 264: 'tryclose branch' 
843706     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 265: 'rule ifthenelse_split occ=0' 
843707     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 266: 'rule getOfSwap' 
843708     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 267: 'rule ifthenelse_negated' 
843709     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 268: 'rule ifthenelse_split occ=0' 
843710     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 269: 'tryclose branch' 
843717     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 270: 'tryclose branch' 
843724     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 271: 'tryclose branch' 
843875     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 272: 'tryclose branch' 
843985     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 273: 'rule getOfSwap' 
843987     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 274: 'rule ifthenelse_negated' 
843988     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 275: 'rule ifthenelse_split occ=0' 
843989     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 276: 'tryclose branch' 
844205     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 277: 'tryclose branch' 
844333     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 278: 'cut 'int::seqGet(s_0, v_y_0)=v_x_0'' 
844334     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 279: 'tryclose branch' 
848256     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 280: 'rule seqNPermSwapNPerm' 
848262     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 281: 'instantiate hide var=iv with='jv_1'' 
848264     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 282: 'instantiate hide var=jv with='v_y_0'' 
848264     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 283: 'rule impLeft' 
848265     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 284: 'tryclose branch' 
848414     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 285: 'rule seqNPermSwapNPerm formula='seqNPerm(seqSwap(s_0,jv_1,v_y_0))'' 
848416     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 286: 'instantiate hide var=iv with='jv_1'' 
848417     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 287: 'instantiate hide var=jv with='v_x_0'' 
848418     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 288: 'rule impLeft' 
848419     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 289: 'tryclose branch' 
848553     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 290: 'tryclose branch' 
852391     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 291: 'tryclose branch' 
856529     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 292: 'rule seqNPermSwapNPerm formula='seqNPerm(s_0)'' 
856536     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 293: 'instantiate hide var=iv with='v_x_0'' 
856537     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 294: 'instantiate hide var=jv with='jv_0'' 
856538     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 295: 'rule impLeft' 
856540     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 296: 'tryclose branch' 
856755     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 297: 'rule seqNPermSwapNPerm formula='seqNPerm(seqSwap(s_0,v_x_0,jv_0))'' 
856757     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 298: 'instantiate hide var=iv with='v_y_0'' 
856758     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 299: 'instantiate hide var=jv with='jv_1'' 
856759     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)' ...' 
856762     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 301: 'tryclose branch' 
858222     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm2/Taclet_schiffl_thm_1.proof 
858222     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 106.7ns 
858223     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
861477     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.25s 
861477     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: schiffl_thm_1 
862566     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: schiffl_thm_1 
862567     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 8.9ns 
862568     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 1: 'macro split-prop' 
862578     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 2: 'rule schiffl_lemma_2 formula='seqPerm(f_s, f_t)'' 
862592     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 3: 'instantiate hide var=x with='f_x'' 
862595     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 4: 'instantiate hide var=y with='f_y'' 
862597     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 5: 'rule impLeft' 
862597     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 6: 'tryclose branch' 
862603     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 7: 'rule exLeft' 
862605     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 8: 'macro split-prop' 
862610     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 9: 'rule seqPermDef occ=1' 
862613     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 10: 'rule andRight' 
862614     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 11: 'tryclose branch' 
862627     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 12: 'instantiate hide var=s with='r_0'' 
862629     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 13: 'rule andRight' 
862630     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 14: 'tryclose branch' 
862775     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 15: 'rule allRight' 
862776     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 16: 'rule impRight' 
862777     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 17: 'instantiate hide var=iv with='iv_0'' 
862778     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 18: 'rule impLeft' 
862778     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 19: 'tryclose branch' 
862878     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 20: 'rule andLeft' 
862878     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 21: 'rule seqNPermRange' 
862880     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 22: 'instantiate hide var=iv with='iv_0'' 
862881     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 23: 'rule impLeft' 
862882     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 24: 'tryclose branch' 
862888     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 25: 'rule andLeft' 
862888     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 26: 'rule andLeft' 
862889     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 27: 'rule seqNPermRange' 
862890     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 28: 'instantiate hide var=iv with='f_x'' 
862891     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 29: 'rule impLeft' 
862892     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 30: 'tryclose branch' 
863008     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 31: 'rule andLeft' 
863010     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 32: 'rule andLeft' 
863010     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 33: 'rule seqNPermRange' 
863012     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 34: 'instantiate hide var=iv with='f_y'' 
863013     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 35: 'rule impLeft' 
863013     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 36: 'tryclose branch' 
863136     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 37: 'rule andLeft' 
863137     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 38: 'rule andLeft' 
863138     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 39: 'rule getOfSeqDef occ=0' 
863138     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 40: 'rule getOfSeqDef' 
863139     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 41: 'rule ifthenelse_split occ=0' 
863140     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 42: 'rule andLeft occ=0' 
863141     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 43: 'rule sub_zero_2 occ=0' 
863142     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 44: 'rule ifthenelse_split occ=2' 
863143     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 45: 'rule andLeft' 
863143     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 46: 'rule sub_zero_2 occ=0' 
863144     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 47: 'rule add_zero_right occ=0' 
863145     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 48: 'rule add_zero_right occ=0' 
863145     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 49: 'rule add_zero_right occ=0' 
863146     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 50: 'rule add_zero_right occ=0' 
863147     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 51: 'rule add_zero_right occ=0' 
863147     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 52: 'rule add_zero_right occ=0' 
863149     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 53: 'rule ifthenelse_split occ=0' 
863150     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 54: 'rule ifthenelse_split occ=0' 
863151     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 55: 'tryclose branch' 
863154     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 56: 'tryclose branch' 
863206     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 57: 'rule ifthenelse_split occ=0' 
863207     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 58: 'tryclose branch' 
863286     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 59: 'rule ifthenelse_split occ=0' 
863288     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 60: 'rule seqNPermInjective' 
863289     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 61: 'instantiate hide var=iv with='iv_0'' 
863292     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 62: 'instantiate hide var=jv with='f_y'' 
863292     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 63: 'rule impLeft' 
863293     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 64: 'tryclose branch' 
863355     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 65: 'tryclose branch' 
863358     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 66: 'rule ifthenelse_split occ=0' 
863360     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 67: 'rule seqNPermInjective' 
863362     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 68: 'instantiate hide var=iv with='iv_0'' 
863363     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 69: 'instantiate hide var=jv with='f_x'' 
863364     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 70: 'rule impLeft' 
863364     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 71: 'tryclose branch' 
863430     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 72: 'tryclose branch' 
863433     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 73: 'tryclose branch' 
863436     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 74: 'tryclose branch' 
863507     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 75: 'tryclose branch' 
863590     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_eqSameSeq.proof 
863591     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 292.2ns 
863592     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
866730     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.14s 
866730     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: eqSameSeq 
867840     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: eqSameSeq 
867890     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 45.85ms