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

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

tests
0

failures
0

ignored
11m3.21s

duration
100%

successful

Tests

Test Method name Duration Result
powPositive data()[100] 3.194s passed
powPositiveConcrete data()[101] 3.190s passed
powGeq1Concrete data()[102] 3.184s passed
pow2InIntLower data()[103] 3.190s passed
pow2InIntUpper data()[104] 3.196s passed
logSelfConcrete data()[105] 3.201s passed
log1Concrete data()[106] 3.204s passed
logProduct data()[107] 3.240s passed
logTimesBaseConcrete data()[108] 3.191s passed
logProdIdentity data()[109] 3.213s passed
moduloByteIsInByte data()[10] 3.277s passed
logProdIdentityConcrete data()[110] 3.193s passed
logPowIdentity data()[111] 3.203s passed
logPowIdentityConcrete data()[112] 3.204s passed
logPositive data()[113] 3.218s passed
logPositiveConcrete data()[114] 3.197s passed
logMono data()[115] 3.226s passed
logMonoConcrete data()[116] 3.204s passed
powLogLess data()[117] 3.229s passed
powLogMore2 data()[118] 3.279s passed
logLessThanPow data()[119] 3.241s passed
moduloCharIsInChar data()[11] 3.252s passed
logLessThanPowConcrete data()[120] 3.228s passed
logSqueeze data()[121] 3.207s passed
ifthenelse_equals data()[122] 3.213s passed
ifthenelse_equals_1 data()[123] 3.202s passed
ifthenelse_equals_2 data()[124] 3.202s passed
disjointWithSingleton1 data()[125] 3.211s passed
disjointWithSingleton2 data()[126] 3.228s passed
disjointArrayRanges data()[127] 3.242s passed
disjointArrayRangeAllFields1 data()[128] 3.217s passed
disjointArrayRangeAllFields2 data()[129] 3.229s passed
div_unique1 data()[12] 3.377s passed
seqSelfDefinition data()[130] 3.237s passed
seqOutsideValue data()[131] 3.201s passed
castedGetAny data()[132] 3.226s passed
seqGetAlphaCast data()[133] 3.240s passed
getOfSeqSingleton data()[134] 3.222s passed
getOfSeqSingletonConcrete data()[135] 3.205s passed
getOfSeqConcat data()[136] 3.217s passed
getOfSeqSub data()[137] 3.206s passed
getOfSeqReverse data()[138] 3.231s passed
lenOfSeqEmpty data()[139] 3.230s passed
div_unique2 data()[13] 3.302s passed
lenOfSeqSingleton data()[140] 3.209s passed
lenOfSeqConcat data()[141] 3.220s passed
lenOfSeqSub data()[142] 3.239s passed
lenOfSeqReverse data()[143] 3.218s passed
equalityToSeqGetAndSeqLenLeft data()[144] 3.212s passed
equalityToSeqGetAndSeqLenRight data()[145] 3.251s passed
getOfSeqSingletonEQ data()[146] 3.229s passed
getOfSeqConcatEQ data()[147] 3.233s passed
getOfSeqSubEQ data()[148] 3.251s passed
getOfSeqReverseEQ data()[149] 3.223s passed
div_exists data()[14] 3.404s passed
lenOfSeqEmptyEQ data()[150] 3.221s passed
lenOfSeqSingletonEQ data()[151] 3.235s passed
lenOfSeqConcatEQ data()[152] 3.234s passed
lenOfSeqSubEQ data()[153] 3.219s passed
lenOfSeqReverseEQ data()[154] 3.237s passed
getOfSeqDefEQ data()[155] 3.226s passed
lenOfSeqDefEQ data()[156] 3.309s passed
seqConcatWithSeqEmpty1 data()[157] 3.234s passed
seqConcatWithSeqEmpty2 data()[158] 3.231s passed
seqReverseOfSeqEmpty data()[159] 3.244s passed
div_one data()[15] 3.262s passed
subSeqComplete data()[160] 3.222s passed
subSeqTailR data()[161] 3.243s passed
subSeqTailL data()[162] 3.215s passed
subSeqTailEQR data()[163] 3.228s passed
subSeqTailEQL data()[164] 3.199s passed
seqDef_split data()[165] 3.247s passed
seqDef_induction_upper data()[166] 3.247s passed
seqDef_induction_upper_concrete data()[167] 3.260s passed
seqDef_induction_lower data()[168] 3.240s passed
seqDef_induction_lower_concrete data()[169] 3.269s passed
jdiv_one data()[16] 3.241s passed
seqDef_split_in_three data()[170] 3.338s passed
seqDef_empty data()[171] 3.219s passed
seqDef_one_summand data()[172] 3.238s passed
seqDef_lower_equals_upper data()[173] 3.198s passed
seqDefOfSeq data()[174] 3.250s passed
seqSelfDefinitionEQ2 data()[175] 3.246s passed
indexOfSeqSingleton data()[176] 3.215s passed
indexOfSeqConcatFirst data()[177] 3.245s passed
indexOfSeqConcatSecond data()[178] 3.247s passed
indexOfSeqSub data()[179] 3.248s passed
div_zero data()[17] 3.306s passed
lenOfArray2seq data()[180] 3.226s passed
getAnyOfArray2seq data()[181] 3.221s passed
getOfArray2seq data()[182] 3.208s passed
getAnyOfNPermInv data()[183] 3.228s passed
seqNPermRange data()[184] 3.280s passed
seqPermTrans data()[185] 3.266s passed
seqPermRefl data()[186] 3.232s passed
seqPermSplit data()[187] 3.222s passed
seqNPermRight data()[188] 3.416s passed
seqPermFromSwap data()[189] 3.279s passed
divResZero1 data()[18] 3.273s passed
seqPermTransAlt0 data()[190] 3.211s passed
seqPermTransAlt1 data()[191] 3.197s passed
seqPermTransAlt2 data()[192] 3.207s passed
seqPermTransAlt3 data()[193] 3.202s passed
seqPermForall data()[194] 3.315s passed
seqPermExists data()[195] 3.289s passed
schiffl_lemma_2 data()[196] 21.308s passed
schiffl_thm_1 data()[197] 4.073s passed
eqSameSeq data()[198] 3.349s passed
divResZero2 data()[19] 3.269s passed
eqTermCut data()[1] 3.847s passed
divResOne1 data()[20] 3.294s passed
divResOne2 data()[21] 3.318s passed
div_cancel1 data()[22] 3.307s passed
div_cancel2 data()[23] 3.261s passed
divAddMultDenom data()[24] 3.290s passed
divMinus data()[25] 3.344s passed
divMinusDenom data()[26] 3.310s passed
divLeastDPos data()[27] 3.267s passed
divLeastDNeg data()[28] 3.253s passed
divGreatestDPos data()[29] 3.227s passed
equivAllRight data()[2] 3.647s passed
divGreatestDNeg data()[30] 3.236s passed
divIncreasingPos data()[31] 3.222s passed
divIncreasingNeg data()[32] 3.245s passed
jdiv_zero data()[33] 3.273s passed
jdivPulloutMinusNum data()[34] 3.239s passed
jdivPulloutMinusDenom data()[35] 3.416s passed
jdiv_uniquePosPos data()[36] 3.270s passed
jdiv_uniquePosNeg data()[37] 3.264s passed
jdiv_uniqueNegPos data()[38] 3.241s passed
jdiv_uniqueNegNeg data()[39] 3.245s passed
irrflConcrete1 data()[3] 3.639s passed
jdivMultDenom1 data()[40] 3.259s passed
jdivMultDenom2 data()[41] 3.235s passed
mod_geZero data()[42] 3.264s passed
mod_lessDenom data()[43] 3.268s passed
jmod_NumPos data()[44] 3.265s passed
jmod_NumNeg data()[45] 3.287s passed
jmod_geZero data()[46] 3.241s passed
jmodNumZero data()[47] 3.256s passed
jmod_pulloutminusNum data()[48] 3.249s passed
jmod_pulloutminusDenom data()[49] 3.230s passed
irrflConcrete2 data()[4] 3.481s passed
jmodUnique1 data()[50] 3.324s passed
jmodUnique2 data()[51] 3.343s passed
intDivRem data()[52] 3.229s passed
jmodjmod data()[53] 3.262s passed
jmodDivisible data()[54] 3.269s passed
jmodDivisibleRep data()[55] 3.235s passed
jdivAddMultDenom data()[56] 3.391s passed
jmodAltZero data()[57] 3.268s passed
jmodAddMultDenomZero data()[58] 3.234s passed
polyDiv_zero data()[59] 3.234s passed
cancel_gtPos data()[5] 3.463s passed
polyMod_ltdivDenom data()[60] 3.238s passed
bsum_empty data()[61] 3.221s passed
bsum_induction_upper data()[62] 3.223s passed
bsum_induction_lower data()[63] 3.251s passed
bsum_num_of_bounds data()[64] 3.285s passed
bsum_num_of_bounds2 data()[65] 3.232s passed
bsum_induction_upper2 data()[66] 3.228s passed
bsum_induction_upper_concrete data()[67] 3.220s passed
bsum_induction_upper_concrete_2 data()[68] 3.236s passed
bsum_induction_upper2_concrete data()[69] 3.218s passed
cancel_gtNeg data()[6] 3.339s passed
bsum_induction_lower_concrete data()[70] 3.206s passed
bsum_induction_lower2 data()[71] 3.214s passed
bsum_induction_lower2_concrete data()[72] 3.198s passed
bsum_positive data()[73] 3.288s passed
bsum_upper_bound data()[74] 3.273s passed
bsum_lower_bound data()[75] 3.279s passed
bsum_positive_lower_bound_element data()[76] 3.244s passed
bsum_sub_same_index data()[77] 3.241s passed
bsum_less_same_index data()[78] 3.263s passed
bsum_equal_except_one_index data()[79] 3.227s passed
moduloIntIsInInt data()[7] 3.299s passed
bsum_num_of_is_max data()[80] 3.229s passed
bsum_num_of_is_max2 data()[81] 3.234s passed
bsum_num_of_is_max3 data()[82] 3.220s passed
bsum_num_of_is_max4 data()[83] 3.220s passed
bsum_num_of_lt_max data()[84] 3.215s passed
bsum_num_of_lt_max2 data()[85] 3.261s passed
bsum_num_of_lt_max3 data()[86] 3.238s passed
bsum_num_of_lt_max4 data()[87] 3.232s passed
bsum_num_of_gt0 data()[88] 3.237s passed
bsum_num_of_gt0_alt data()[89] 3.217s passed
moduloLongIsInLong data()[8] 3.325s passed
bsum_add_concrete data()[90] 3.204s passed
bprod_all_positive data()[91] 3.217s passed
bprod_split data()[92] 3.200s passed
powConcrete0 data()[93] 3.210s passed
powConcrete1 data()[94] 3.200s passed
powSplitFactor data()[95] 3.217s passed
powAdd data()[96] 3.237s passed
powMono data()[97] 3.224s passed
powMonoConcrete data()[98] 3.213s passed
powMonoConcreteRight data()[99] 3.204s passed
moduloShortIsInShort data()[9] 3.318s passed

Standard output

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

1553       DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for Meta 
1564       DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for Meta 
1567       DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for Meta 
1570       DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for Meta 
2844       DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for JavaBigintExpression 
8567       DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 8.03s 
8629       INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof dummyTrue.key 
8664       DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 38ns 
8680       INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/firstOrder/Taclet_eqTermCut.proof 
8681       DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 734.31ns 
8686       INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
11528      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.84s 
11530      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: eqTermCut 
12491      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: eqTermCut 
12515      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 18.74ms 
12529      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/firstOrder/Taclet_equivAllRight.proof 
12529      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 206.4ns 
12530      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
15305      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.77s 
15305      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: equivAllRight 
16158      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: equivAllRight 
16173      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 10.92ms 
16175      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_irrflConcrete1.proof 
16176      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 166.5ns 
16177      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
18898      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.72s 
18899      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: irrflConcrete1 
19804      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: irrflConcrete1 
19812      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.59ms 
19816      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_irrflConcrete2.proof 
19816      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 173.4ns 
19817      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
22381      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.56s 
22382      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: irrflConcrete2 
23278      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: irrflConcrete2 
23293      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 9.84ms 
23299      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_cancel_gtPos.proof 
23300      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 549.71ns 
23302      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
25845      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.54s 
25845      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: cancel_gtPos 
26684      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: cancel_gtPos 
26756      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 62.59ms 
26764      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_cancel_gtNeg.proof 
26764      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 176.9ns 
26765      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
29262      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.5s 
29262      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: cancel_gtNeg 
30081      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: cancel_gtNeg 
30100      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 16.21ms 
30102      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intRulesIgnoringOF/Taclet_moduloIntIsInInt.proof 
30102      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 126.5ns 
30103      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
32581      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.48s 
32581      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: moduloIntIsInInt 
33395      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: moduloIntIsInInt 
33399      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 817.32ns 
33401      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intRulesIgnoringOF/Taclet_moduloLongIsInLong.proof 
33402      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 338.61ns 
33403      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
35892      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.49s 
35893      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: moduloLongIsInLong 
36722      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: moduloLongIsInLong 
36725      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 578.91ns 
36728      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intRulesIgnoringOF/Taclet_moduloShortIsInShort.proof 
36728      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 348.61ns 
36729      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
39247      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.52s 
39247      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: moduloShortIsInShort 
40041      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: moduloShortIsInShort 
40044      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 620.21ns 
40045      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intRulesIgnoringOF/Taclet_moduloByteIsInByte.proof 
40045      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 107ns 
40046      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
42535      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.49s 
42536      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: moduloByteIsInByte 
43318      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: moduloByteIsInByte 
43320      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 626.81ns 
43322      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intRulesIgnoringOF/Taclet_moduloCharIsInChar.proof 
43322      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 123ns 
43323      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
45786      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.46s 
45786      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: moduloCharIsInChar 
46569      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: moduloCharIsInChar 
46572      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 563.21ns 
46575      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_div_unique1.proof 
46575      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 566.61ns 
46576      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
49075      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.5s 
49075      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: div_unique1 
49908      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: div_unique1 
49949      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 37.72ms 
49951      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_div_unique2.proof 
49952      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 151.5ns 
49954      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
52408      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.45s 
52408      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: div_unique2 
53213      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: div_unique2 
53251      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 34.41ms 
53254      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_div_exists.proof 
53254      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 367.11ns 
53255      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
55702      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.45s 
55702      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: div_exists 
56504      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: div_exists 
56654      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 141.51ms 
56658      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_div_one.proof 
56658      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 450.91ns 
56659      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
59107      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.45s 
59108      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: div_one 
59911      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: div_one 
59917      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.01ms 
59919      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdiv_one.proof 
59920      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 362.11ns 
59921      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
62351      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.43s 
62352      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdiv_one 
63154      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdiv_one 
63157      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.37ms 
63161      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_div_zero.proof 
63161      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 350.71ns 
63163      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
65625      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.46s 
65626      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: div_zero 
66426      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: div_zero 
66464      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 33.59ms 
66467      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divResZero1.proof 
66467      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 353.01ns 
66469      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
68920      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.45s 
68921      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divResZero1 
69722      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divResZero1 
69738      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 12.11ms 
69740      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divResZero2.proof 
69740      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 211.9ns 
69741      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
72185      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.44s 
72186      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divResZero2 
72992      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divResZero2 
73007      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 11.01ms 
73010      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divResOne1.proof 
73010      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 384.81ns 
73011      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
75491      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.48s 
75492      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divResOne1 
76278      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divResOne1 
76301      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 19.15ms 
76303      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divResOne2.proof 
76303      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 145.8ns 
76304      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
78820      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.52s 
78821      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divResOne2 
79605      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divResOne2 
79619      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 11.88ms 
79621      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_div_cancel1.proof 
79621      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 130.2ns 
79622      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
82114      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.49s 
82115      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: div_cancel1 
82901      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: div_cancel1 
82925      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 19.78ms 
82928      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_div_cancel2.proof 
82928      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 345.81ns 
82929      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
85380      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.45s 
85380      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: div_cancel2 
86185      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: div_cancel2 
86188      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.09ms 
86189      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divAddMultDenom.proof 
86189      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 98.5ns 
86190      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
88635      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.44s 
88635      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divAddMultDenom 
89438      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divAddMultDenom 
89477      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 33.16ms 
89478      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divMinus.proof 
89479      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 143.6ns 
89480      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
91934      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.45s 
91935      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divMinus 
92755      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divMinus 
92820      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 56.57ms 
92823      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divMinusDenom.proof 
92824      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 351.71ns 
92825      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
95285      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.46s 
95285      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divMinusDenom 
96089      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divMinusDenom 
96132      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 37.7ms 
96134      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divLeastDPos.proof 
96134      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 129.2ns 
96135      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
98591      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.46s 
98591      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divLeastDPos 
99392      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divLeastDPos 
99399      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 5.14ms 
99400      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divLeastDNeg.proof 
99401      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 120.9ns 
99401      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
101840     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.44s 
101841     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divLeastDNeg 
102640     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divLeastDNeg 
102652     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 9.68ms 
102653     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divGreatestDPos.proof 
102653     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 120.2ns 
102654     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
105075     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.42s 
105075     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divGreatestDPos 
105868     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divGreatestDPos 
105879     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 8.65ms 
105881     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divGreatestDNeg.proof 
105882     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 205ns 
105882     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
108326     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.44s 
108327     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divGreatestDNeg 
109107     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divGreatestDNeg 
109115     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 5.34ms 
109116     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divIncreasingPos.proof 
109116     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 104.9ns 
109117     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
111555     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.44s 
111555     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divIncreasingPos 
112330     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divIncreasingPos 
112337     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 5ms 
112339     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divIncreasingNeg.proof 
112339     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 111.4ns 
112340     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
114801     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.46s 
114801     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divIncreasingNeg 
115575     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divIncreasingNeg 
115582     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.65ms 
115583     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdiv_zero.proof 
115584     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 125.2ns 
115584     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
118044     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.46s 
118045     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdiv_zero 
118851     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdiv_zero 
118855     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.43ms 
118856     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdivPulloutMinusNum.proof 
118857     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 172.2ns 
118857     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
121290     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.43s 
121290     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdivPulloutMinusNum 
122084     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdivPulloutMinusNum 
122094     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 7.76ms 
122096     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdivPulloutMinusDenom.proof 
122096     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 197.8ns 
122097     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
124575     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.48s 
124578     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdivPulloutMinusDenom 
125422     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdivPulloutMinusDenom 
125507     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 78.15ms 
125512     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdiv_uniquePosPos.proof 
125513     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 458.41ns 
125514     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
127963     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.45s 
127963     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdiv_uniquePosPos 
128762     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdiv_uniquePosPos 
128779     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 14.11ms 
128784     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdiv_uniquePosNeg.proof 
128784     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 223.4ns 
128785     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
131227     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.44s 
131228     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdiv_uniquePosNeg 
132026     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdiv_uniquePosNeg 
132044     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 15.37ms 
132046     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdiv_uniqueNegPos.proof 
132046     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 97.7ns 
132047     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
134473     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.43s 
134473     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdiv_uniqueNegPos 
135268     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdiv_uniqueNegPos 
135286     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 14.82ms 
135287     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdiv_uniqueNegNeg.proof 
135287     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 102.7ns 
135288     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
137717     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.43s 
137718     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdiv_uniqueNegNeg 
138513     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdiv_uniqueNegNeg 
138530     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 13.84ms 
138531     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdivMultDenom1.proof 
138531     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 97.3ns 
138532     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
140954     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.42s 
140954     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdivMultDenom1 
141749     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdivMultDenom1 
141789     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 35.52ms 
141791     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdivMultDenom2.proof 
141791     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 86.2ns 
141792     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
144247     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.46s 
144248     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdivMultDenom2 
145021     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdivMultDenom2 
145024     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.03ms 
145025     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_mod_geZero.proof 
145025     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 73.4ns 
145026     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
147487     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.46s 
147487     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: mod_geZero 
148283     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: mod_geZero 
148288     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.5ms 
148290     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_mod_lessDenom.proof 
148291     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 313.4ns 
148292     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
150775     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.48s 
150775     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: mod_lessDenom 
151548     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: mod_lessDenom 
151556     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 5.77ms 
151557     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmod_NumPos.proof 
151558     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 85.1ns 
151558     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
154012     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.45s 
154012     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmod_NumPos 
154812     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmod_NumPos 
154821     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 6.29ms 
154822     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmod_NumNeg.proof 
154822     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 86.5ns 
154823     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
157289     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.47s 
157290     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmod_NumNeg 
158089     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmod_NumNeg 
158108     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 16.33ms 
158109     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmod_geZero.proof 
158109     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 106.6ns 
158110     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
160542     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.43s 
160543     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmod_geZero 
161340     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmod_geZero 
161348     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 5.99ms 
161351     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmodNumZero.proof 
161351     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 299.31ns 
161352     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
163785     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.43s 
163785     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmodNumZero 
164602     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmodNumZero 
164605     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.37ms 
164608     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmod_pulloutminusNum.proof 
164608     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 96.8ns 
164608     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
167050     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.44s 
167050     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmod_pulloutminusNum 
167850     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmod_pulloutminusNum 
167855     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.94ms 
167856     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmod_pulloutminusDenom.proof 
167856     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 79.2ns 
167857     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
170288     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.43s 
170288     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmod_pulloutminusDenom 
171081     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmod_pulloutminusDenom 
171085     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.45ms 
171086     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmodUnique1.proof 
171086     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 84.6ns 
171087     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
173504     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.42s 
173504     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmodUnique1 
174306     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmodUnique1 
174407     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 92.78ms 
174411     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmodUnique2.proof 
174411     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 181.2ns 
174412     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
176856     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.44s 
176857     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmodUnique2 
177657     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmodUnique2 
177751     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 85.94ms 
177759     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_intDivRem.proof 
177759     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 364.21ns 
177760     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
180212     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.45s 
180212     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: intDivRem 
180982     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: intDivRem 
180986     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.65ms 
180987     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmodjmod.proof 
180987     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 144.4ns 
180988     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
183438     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.45s 
183438     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmodjmod 
184211     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmodjmod 
184247     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 32.93ms 
184248     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmodDivisible.proof 
184249     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 129.1ns 
184249     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
186690     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.44s 
186690     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmodDivisible 
187488     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmodDivisible 
187516     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 25.49ms 
187518     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmodDivisibleRep.proof 
187518     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 92.2ns 
187519     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
189952     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.43s 
189952     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmodDivisibleRep 
190748     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmodDivisibleRep 
190751     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.17ms 
190752     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdivAddMultDenom.proof 
190753     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 65.5ns 
190754     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
193191     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.44s 
193192     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdivAddMultDenom 
193995     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdivAddMultDenom 
194141     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 136.39ms 
194143     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmodAltZero.proof 
194144     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 101ns 
194144     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
196595     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.45s 
196595     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmodAltZero 
197399     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmodAltZero 
197410     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 8.7ms 
197413     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmodAddMultDenomZero.proof 
197413     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 288.61ns 
197414     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
199844     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.43s 
199844     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmodAddMultDenomZero 
200637     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmodAddMultDenomZero 
200645     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 5.85ms 
200646     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_polyDiv_zero.proof 
200646     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 88ns 
200647     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
203065     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.42s 
203065     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: polyDiv_zero 
203861     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: polyDiv_zero 
203878     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 14.28ms 
203879     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_polyMod_ltdivDenom.proof 
203880     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 95.1ns 
203880     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
206307     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.43s 
206308     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: polyMod_ltdivDenom 
207103     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: polyMod_ltdivDenom 
207116     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 6.53ms 
207118     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_empty.proof 
207118     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 90.2ns 
207119     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
209558     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.44s 
209558     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_empty 
210333     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_empty 
210337     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.6ms 
210338     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_induction_upper.proof 
210338     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 109.7ns 
210339     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
212782     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.44s 
212783     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_upper 
213555     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_induction_upper 
213560     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.05ms 
213563     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_induction_lower.proof 
213563     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 107.7ns 
213564     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
216015     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.45s 
216015     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_lower 
216790     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_induction_lower 
216812     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 19.78ms 
216815     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_bounds.proof 
216816     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 380.81ns 
216818     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
219276     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.46s 
219276     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_bounds 
220055     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_bounds 
220072     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 13.13ms 
220099     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_bounds2.proof 
220099     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 104ns 
220100     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
222518     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.42s 
222518     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_bounds2 
223313     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_bounds2 
223329     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 12.91ms 
223331     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_induction_upper2.proof 
223332     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 269.7ns 
223333     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
225760     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.43s 
225760     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_upper2 
226553     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_induction_upper2 
226557     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.68ms 
226559     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_induction_upper_concrete.proof 
226559     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 82.4ns 
226559     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
228979     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.42s 
228979     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_upper_concrete 
229773     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_induction_upper_concrete 
229777     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.6ms 
229779     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_induction_upper_concrete_2.proof 
229779     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 97.7ns 
229780     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
232204     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.42s 
232205     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_upper_concrete_2 
233007     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_induction_upper_concrete_2 
233013     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.89ms 
233014     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_induction_upper2_concrete.proof 
233014     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 111.2ns 
233015     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
235433     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.42s 
235433     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_upper2_concrete 
236229     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_induction_upper2_concrete 
236232     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.46ms 
236233     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_induction_lower_concrete.proof 
236233     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 64.5ns 
236234     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
238639     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.41s 
238640     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_lower_concrete 
239436     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_induction_lower_concrete 
239438     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 665.61ns 
239439     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_induction_lower2.proof 
239439     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 73.2ns 
239440     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
241851     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.41s 
241851     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_lower2 
242647     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_induction_lower2 
242651     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.25ms 
242652     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_induction_lower2_concrete.proof 
242652     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 80.1ns 
242653     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
245056     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.4s 
245057     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_lower2_concrete 
245847     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_induction_lower2_concrete 
245849     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 941.92ns 
245851     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_positive.proof 
245851     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 80.9ns 
245852     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
248282     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.43s 
248282     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_positive 
249063     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_positive 
249137     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 69.4ms 
249139     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_upper_bound.proof 
249139     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 90.4ns 
249142     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
251602     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.46s 
251602     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_upper_bound 
252368     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_upper_bound 
252410     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 39.38ms 
252412     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_lower_bound.proof 
252412     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 69.8ns 
252413     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
254856     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.44s 
254856     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_lower_bound 
255654     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_lower_bound 
255689     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 32.25ms 
255690     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_positive_lower_bound_element.proof 
255690     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 81ns 
255691     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
258096     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.4s 
258096     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_positive_lower_bound_element 
258885     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_positive_lower_bound_element 
258933     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 44.15ms 
258935     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_sub_same_index.proof 
258935     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 84.4ns 
258936     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
261352     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.42s 
261352     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_sub_same_index 
262142     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_sub_same_index 
262174     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 29.13ms 
262175     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_less_same_index.proof 
262175     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 80.8ns 
262176     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
264580     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.4s 
264580     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_less_same_index 
265368     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_less_same_index 
265436     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 63.57ms 
265439     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_equal_except_one_index.proof 
265440     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 227.1ns 
265442     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
267848     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.41s 
267848     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_equal_except_one_index 
268639     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_equal_except_one_index 
268664     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 22.31ms 
268665     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_is_max.proof 
268666     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 84.9ns 
268667     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
271079     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.41s 
271079     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_is_max 
271874     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_is_max 
271893     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 16.25ms 
271895     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_is_max2.proof 
271895     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 88ns 
271896     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
274311     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.41s 
274311     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_is_max2 
275103     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_is_max2 
275127     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 20.18ms 
275129     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_is_max3.proof 
275129     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 207.2ns 
275130     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
277561     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.43s 
277562     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_is_max3 
278328     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_is_max3 
278347     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 15.86ms 
278349     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_is_max4.proof 
278349     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 208.4ns 
278350     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
280774     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.42s 
280774     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_is_max4 
281541     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_is_max4 
281568     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 23.8ms 
281570     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_lt_max.proof 
281570     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 86.5ns 
281571     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
283990     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.42s 
283991     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_lt_max 
284757     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_lt_max 
284782     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 21.74ms 
284783     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_lt_max2.proof 
284784     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 87.8ns 
284784     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
287226     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.44s 
287226     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_lt_max2 
288018     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_lt_max2 
288043     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 21.62ms 
288044     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_lt_max3.proof 
288044     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 86ns 
288045     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
290463     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.42s 
290463     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_lt_max3 
291257     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_lt_max3 
291281     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 21.41ms 
291283     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_lt_max4.proof 
291283     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 83.3ns 
291283     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
293698     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.41s 
293698     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_lt_max4 
294493     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_lt_max4 
294513     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 17.64ms 
294515     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_gt0.proof 
294515     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 78.2ns 
294516     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
296928     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.41s 
296929     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_gt0 
297725     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_gt0 
297750     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 22.07ms 
297751     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_gt0_alt.proof 
297752     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 87.1ns 
297752     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
300153     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.4s 
300153     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_gt0_alt 
300942     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_gt0_alt 
300967     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 22.07ms 
300969     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_add_concrete.proof 
300969     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 85.8ns 
300969     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
303373     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.4s 
303373     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_add_concrete 
304163     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_add_concrete 
304171     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 5.58ms 
304172     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bprod/Taclet_bprod_all_positive.proof 
304172     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 72.5ns 
304173     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
306575     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.4s 
306575     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bprod_all_positive 
307371     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bprod_all_positive 
307388     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 14.65ms 
307389     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bprod/Taclet_bprod_split.proof 
307389     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 66ns 
307390     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
309817     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.43s 
309817     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bprod_split 
310585     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bprod_split 
310589     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.85ms 
310590     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powConcrete0.proof 
310590     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 69.9ns 
310591     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
313023     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.43s 
313024     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powConcrete0 
313796     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powConcrete0 
313799     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 667.61ns 
313800     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powConcrete1.proof 
313800     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 58.3ns 
313801     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
316226     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.43s 
316226     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powConcrete1 
316996     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powConcrete1 
316998     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 749.51ns 
316999     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powSplitFactor.proof 
316999     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 70.5ns 
317000     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
319436     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.44s 
319436     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powSplitFactor 
320208     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powSplitFactor 
320215     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.77ms 
320216     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powAdd.proof 
320216     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 65.1ns 
320217     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
322652     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.43s 
322652     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powAdd 
323446     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powAdd 
323453     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.25ms 
323454     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powMono.proof 
323454     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 65.2ns 
323455     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
325870     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.42s 
325870     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powMono 
326664     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powMono 
326676     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 10.05ms 
326678     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powMonoConcrete.proof 
326678     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 76.6ns 
326678     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
329087     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.41s 
329087     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powMonoConcrete 
329886     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powMonoConcrete 
329890     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.01ms 
329891     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powMonoConcreteRight.proof 
329891     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 63.5ns 
329892     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
332297     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.4s 
332297     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powMonoConcreteRight 
333091     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powMonoConcreteRight 
333093     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 528.21ns 
333094     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powPositive.proof 
333094     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 67.3ns 
333095     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
335491     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.4s 
335491     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powPositive 
336282     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powPositive 
336287     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.45ms 
336288     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powPositiveConcrete.proof 
336288     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 56.2ns 
336289     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
338685     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.4s 
338685     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powPositiveConcrete 
339475     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powPositiveConcrete 
339477     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 584.21ns 
339479     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powGeq1Concrete.proof 
339479     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 56.3ns 
339479     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
341870     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.39s 
341870     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powGeq1Concrete 
342659     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powGeq1Concrete 
342661     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 610.41ns 
342662     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_pow2InIntLower.proof 
342662     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 72.7ns 
342663     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
345060     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.4s 
345061     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: pow2InIntLower 
345849     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: pow2InIntLower 
345852     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 610.91ns 
345853     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_pow2InIntUpper.proof 
345853     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 67.9ns 
345853     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
348272     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.42s 
348272     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: pow2InIntUpper 
349043     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: pow2InIntUpper 
349047     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.11ms 
349048     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logSelfConcrete.proof 
349048     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 67.7ns 
349049     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
351472     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.42s 
351472     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logSelfConcrete 
352239     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logSelfConcrete 
352249     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 7.23ms 
352250     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_log1Concrete.proof 
352250     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 69.8ns 
352251     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
354681     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.43s 
354682     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: log1Concrete 
355449     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: log1Concrete 
355453     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.44ms 
355454     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logProduct.proof 
355454     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 71.3ns 
355455     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
357893     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.44s 
357893     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logProduct 
358686     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logProduct 
358693     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 5.1ms 
358694     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logTimesBaseConcrete.proof 
358694     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 65ns 
358695     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
361090     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.39s 
361090     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logTimesBaseConcrete 
361879     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logTimesBaseConcrete 
361884     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.35ms 
361885     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logProdIdentity.proof 
361885     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 74.7ns 
361886     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
364290     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.4s 
364290     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logProdIdentity 
365081     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logProdIdentity 
365097     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 12.89ms 
365098     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logProdIdentityConcrete.proof 
365098     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 75.2ns 
365099     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
367497     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.4s 
367497     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logProdIdentityConcrete 
368286     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logProdIdentityConcrete 
368289     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.73ms 
368290     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logPowIdentity.proof 
368291     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 86.8ns 
368291     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
370694     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.4s 
370694     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logPowIdentity 
371489     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logPowIdentity 
371492     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.21ms 
371493     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logPowIdentityConcrete.proof 
371493     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 61.2ns 
371494     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
373900     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.41s 
373901     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logPowIdentityConcrete 
374692     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logPowIdentityConcrete 
374696     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.96ms 
374697     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logPositive.proof 
374697     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 55.4ns 
374698     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
377100     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.4s 
377100     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logPositive 
377896     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logPositive 
377914     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 14.71ms 
377915     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logPositiveConcrete.proof 
377915     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 76.3ns 
377916     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
380318     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.4s 
380318     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logPositiveConcrete 
381106     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logPositiveConcrete 
381111     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 540.31ns 
381112     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logMono.proof 
381112     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 80.9ns 
381113     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
383531     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.42s 
383532     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logMono 
384300     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logMono 
384338     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 33.95ms 
384339     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logMonoConcrete.proof 
384339     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 84.1ns 
384340     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
386769     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.43s 
386769     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logMonoConcrete 
387538     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logMonoConcrete 
387541     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.73ms 
387543     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powLogLess.proof 
387543     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 64.7ns 
387544     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
389977     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.43s 
389977     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powLogLess 
390747     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powLogLess 
390770     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 20.52ms 
390773     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powLogMore2.proof 
390773     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 84.7ns 
390773     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
393233     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.46s 
393233     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powLogMore2 
394029     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powLogMore2 
394049     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 17.84ms 
394050     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logLessThanPow.proof 
394050     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 84.5ns 
394051     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
396473     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.42s 
396473     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logLessThanPow 
397266     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logLessThanPow 
397290     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 21.02ms 
397292     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logLessThanPowConcrete.proof 
397292     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 71.5ns 
397292     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
399721     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.43s 
399721     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logLessThanPowConcrete 
400516     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logLessThanPowConcrete 
400518     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 602.91ns 
400520     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logSqueeze.proof 
400520     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 238.7ns 
400521     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
402929     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.41s 
402929     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logSqueeze 
403719     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logSqueeze 
403725     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.94ms 
403726     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/booleanRules/Taclet_ifthenelse_equals.proof 
403726     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 63.2ns 
403727     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
406135     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.41s 
406135     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: ifthenelse_equals 
406935     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: ifthenelse_equals 
406938     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.37ms 
406940     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/booleanRules/Taclet_ifthenelse_equals_1.proof 
406940     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 67.7ns 
406940     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
409343     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.4s 
409344     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: ifthenelse_equals_1 
410137     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: ifthenelse_equals_1 
410140     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 824.51ns 
410141     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/booleanRules/Taclet_ifthenelse_equals_2.proof 
410141     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 68.9ns 
410142     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
412547     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.4s 
412547     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: ifthenelse_equals_2 
413340     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: ifthenelse_equals_2 
413343     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 930.02ns 
413344     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/locSet/Taclet_disjointWithSingleton1.proof 
413344     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 55.8ns 
413345     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
415777     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.43s 
415777     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: disjointWithSingleton1 
416549     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: disjointWithSingleton1 
416553     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.81ms 
416554     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/locSet/Taclet_disjointWithSingleton2.proof 
416554     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 53.2ns 
416555     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
419000     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.44s 
419000     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: disjointWithSingleton2 
419778     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: disjointWithSingleton2 
419781     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.51ms 
419783     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/locSet/Taclet_disjointArrayRanges.proof 
419783     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 128.5ns 
419784     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
422215     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.43s 
422216     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: disjointArrayRanges 
423014     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: disjointArrayRanges 
423024     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 7.3ms 
423025     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/locSet/Taclet_disjointArrayRangeAllFields1.proof 
423025     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 61ns 
423026     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
425432     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.41s 
425432     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: disjointArrayRangeAllFields1 
426228     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: disjointArrayRangeAllFields1 
426241     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 10.91ms 
426242     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/locSet/Taclet_disjointArrayRangeAllFields2.proof 
426242     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 60.8ns 
426243     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
428650     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.41s 
428651     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: disjointArrayRangeAllFields2 
429453     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: disjointArrayRangeAllFields2 
429469     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 14.16ms 
429474     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqSelfDefinition.proof 
429474     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 92.1ns 
429475     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
431888     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.41s 
431888     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqSelfDefinition 
432691     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqSelfDefinition 
432706     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 12.77ms 
432707     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqOutsideValue.proof 
432707     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 79.6ns 
432708     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
435101     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.39s 
435101     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqOutsideValue 
435903     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqOutsideValue 
435907     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.83ms 
435909     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_castedGetAny.proof 
435909     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 71.3ns 
435909     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
438336     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.43s 
438337     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: castedGetAny 
439122     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: castedGetAny 
439133     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 8.78ms 
439135     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqGetAlphaCast.proof 
439135     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 203.7ns 
439136     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
441567     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.43s 
441567     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqGetAlphaCast 
442371     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqGetAlphaCast 
442373     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 682.81ns 
442374     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqSingleton.proof 
442374     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 69.8ns 
442375     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
444787     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.41s 
444787     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqSingleton 
445592     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqSingleton 
445595     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.42ms 
445596     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqSingletonConcrete.proof 
445596     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 59.3ns 
445597     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
447993     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.4s 
447993     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqSingletonConcrete 
448798     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqSingletonConcrete 
448800     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 811.22ns 
448801     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqConcat.proof 
448801     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 65.9ns 
448802     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
451201     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.4s 
451201     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqConcat 
452006     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqConcat 
452017     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 9.14ms 
452018     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqSub.proof 
452018     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 74.4ns 
452019     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
454439     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.42s 
454440     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqSub 
455219     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqSub 
455223     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.5ms 
455224     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqReverse.proof 
455224     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 68ns 
455225     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
457645     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.42s 
457645     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqReverse 
458448     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqReverse 
458454     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 5.01ms 
458456     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqEmpty.proof 
458456     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 68ns 
458456     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
460874     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.42s 
460874     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqEmpty 
461682     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqEmpty 
461685     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 776.11ns 
461686     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqSingleton.proof 
461686     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 57.2ns 
461687     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
464086     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.4s 
464087     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqSingleton 
464892     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqSingleton 
464894     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 727.61ns 
464895     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqConcat.proof 
464895     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 65.9ns 
464896     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
467328     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.43s 
467328     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqConcat 
468110     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqConcat 
468114     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.23ms 
468115     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqSub.proof 
468115     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 68.5ns 
468116     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
470546     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.43s 
470546     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqSub 
471349     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqSub 
471352     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.44ms 
471354     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqReverse.proof 
471354     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 55.6ns 
471354     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
473762     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.41s 
473762     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqReverse 
474567     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqReverse 
474571     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.59ms 
474572     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_equalityToSeqGetAndSeqLenLeft.proof 
474572     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 56.2ns 
474573     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
476971     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.4s 
476972     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: equalityToSeqGetAndSeqLenLeft 
477780     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: equalityToSeqGetAndSeqLenLeft 
477782     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.41ms 
477784     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_equalityToSeqGetAndSeqLenRight.proof 
477784     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 54.1ns 
477784     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
480221     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.44s 
480221     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: equalityToSeqGetAndSeqLenRight 
481028     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: equalityToSeqGetAndSeqLenRight 
481033     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.85ms 
481034     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqSingletonEQ.proof 
481034     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 56.8ns 
481035     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
483450     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.41s 
483450     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqSingletonEQ 
484259     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqSingletonEQ 
484262     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.68ms 
484264     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqConcatEQ.proof 
484264     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 71.5ns 
484264     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
486677     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.41s 
486677     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqConcatEQ 
487484     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqConcatEQ 
487495     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 8.87ms 
487496     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqSubEQ.proof 
487496     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 63.4ns 
487497     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
489930     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.43s 
489930     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqSubEQ 
490744     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqSubEQ 
490746     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 690.81ns 
490747     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqReverseEQ.proof 
490747     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 65.6ns 
490748     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
493156     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.41s 
493156     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqReverseEQ 
493962     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqReverseEQ 
493969     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 5.11ms 
493970     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqEmptyEQ.proof 
493971     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 70.5ns 
493971     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
496382     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.41s 
496382     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqEmptyEQ 
497188     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqEmptyEQ 
497190     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 946.52ns 
497192     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqSingletonEQ.proof 
497192     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 56.4ns 
497192     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
499620     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.43s 
499620     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqSingletonEQ 
500423     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqSingletonEQ 
500425     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 817.72ns 
500427     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqConcatEQ.proof 
500427     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 66.6ns 
500427     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
502847     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.42s 
502847     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqConcatEQ 
503654     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqConcatEQ 
503660     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.42ms 
503661     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqSubEQ.proof 
503661     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 65.6ns 
503662     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
506093     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.43s 
506093     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqSubEQ 
506876     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqSubEQ 
506879     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.62ms 
506880     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqReverseEQ.proof 
506880     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 71.4ns 
506881     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
509305     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.42s 
509305     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqReverseEQ 
510112     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqReverseEQ 
510115     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.96ms 
510117     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqDefEQ.proof 
510117     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 73.4ns 
510117     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
512532     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.41s 
512532     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqDefEQ 
513338     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqDefEQ 
513342     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.2ms 
513343     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqDefEQ.proof 
513343     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 59.4ns 
513344     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
515788     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.44s 
515788     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqDefEQ 
516618     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqDefEQ 
516650     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 30.87ms 
516652     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqConcatWithSeqEmpty1.proof 
516652     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 76.4ns 
516653     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
519062     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.41s 
519062     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqConcatWithSeqEmpty1 
519869     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqConcatWithSeqEmpty1 
519884     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 13.09ms 
519886     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqConcatWithSeqEmpty2.proof 
519886     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 74.9ns 
519886     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
522316     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.43s 
522317     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqConcatWithSeqEmpty2 
523100     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqConcatWithSeqEmpty2 
523116     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 14.04ms 
523117     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqReverseOfSeqEmpty.proof 
523117     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 75ns 
523118     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
525545     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.43s 
525545     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqReverseOfSeqEmpty 
526349     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqReverseOfSeqEmpty 
526359     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 8.65ms 
526361     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_subSeqComplete.proof 
526361     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 67.4ns 
526361     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
528760     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.4s 
528760     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: subSeqComplete 
529570     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: subSeqComplete 
529581     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 9.03ms 
529582     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_subSeqTailR.proof 
529582     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 75.3ns 
529583     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
531995     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.41s 
531995     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: subSeqTailR 
532796     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: subSeqTailR 
532824     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 25.52ms 
532825     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_subSeqTailL.proof 
532825     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 71ns 
532826     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
535212     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.39s 
535212     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: subSeqTailL 
536014     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: subSeqTailL 
536039     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 22.61ms 
536040     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_subSeqTailEQR.proof 
536040     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 76.4ns 
536041     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
538446     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.41s 
538446     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: subSeqTailEQR 
539244     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: subSeqTailEQR 
539267     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 20.94ms 
539268     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_subSeqTailEQL.proof 
539268     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 76.8ns 
539269     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
541649     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.38s 
541650     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: subSeqTailEQL 
542452     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: subSeqTailEQL 
542466     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 12.09ms 
542468     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDef_split.proof 
542468     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 76.6ns 
542468     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
544882     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.41s 
544882     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_split 
545684     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDef_split 
545713     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 26.53ms 
545715     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDef_induction_upper.proof 
545715     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 62.1ns 
545716     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
548108     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.39s 
548108     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_induction_upper 
548912     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDef_induction_upper 
548960     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 45.37ms 
548962     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDef_induction_upper_concrete.proof 
548962     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 75.7ns 
548962     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
551380     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.42s 
551381     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_induction_upper_concrete 
552183     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDef_induction_upper_concrete 
552220     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 34.75ms 
552222     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDef_induction_lower.proof 
552222     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 74.8ns 
552223     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
554637     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.41s 
554638     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_induction_lower 
555418     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDef_induction_lower 
555461     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 39.15ms 
555462     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDef_induction_lower_concrete.proof 
555462     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 79.8ns 
555463     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
557881     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.42s 
557881     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_induction_lower_concrete 
558685     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDef_induction_lower_concrete 
558729     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 41.12ms 
558730     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDef_split_in_three.proof 
558730     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 70.5ns 
558731     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
561145     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.41s 
561145     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_split_in_three 
561949     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDef_split_in_three 
562067     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 112.01ms 
562068     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDef_empty.proof 
562068     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 71.7ns 
562069     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
564474     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.4s 
564474     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_empty 
565278     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDef_empty 
565286     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 5.89ms 
565287     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDef_one_summand.proof 
565287     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 61.8ns 
565288     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
567710     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.42s 
567710     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_one_summand 
568517     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDef_one_summand 
568524     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 5.67ms 
568526     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDef_lower_equals_upper.proof 
568526     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 76.2ns 
568527     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
570935     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.41s 
570935     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_lower_equals_upper 
571717     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDef_lower_equals_upper 
571722     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.56ms 
571723     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDefOfSeq.proof 
571723     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 68.7ns 
571724     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
574150     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.43s 
574151     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDefOfSeq 
574955     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDefOfSeq 
574973     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 14.98ms 
574974     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqSelfDefinitionEQ2.proof 
574974     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 75.9ns 
574975     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
577402     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.43s 
577402     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqSelfDefinitionEQ2 
578207     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqSelfDefinitionEQ2 
578218     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 8.75ms 
578219     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_indexOfSeqSingleton.proof 
578219     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 59.5ns 
578220     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
580625     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.4s 
580625     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: indexOfSeqSingleton 
581430     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: indexOfSeqSingleton 
581434     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.7ms 
581435     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_indexOfSeqConcatFirst.proof 
581435     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 67.7ns 
581436     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
583855     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.42s 
583855     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: indexOfSeqConcatFirst 
584662     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: indexOfSeqConcatFirst 
584678     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 14.5ms 
584680     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_indexOfSeqConcatSecond.proof 
584680     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 75.3ns 
584681     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
587104     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.42s 
587104     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: indexOfSeqConcatSecond 
587909     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: indexOfSeqConcatSecond 
587925     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 13.83ms 
587927     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_indexOfSeqSub.proof 
587927     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 61.6ns 
587927     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
590348     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.42s 
590348     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: indexOfSeqSub 
591154     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: indexOfSeqSub 
591173     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 16.34ms 
591175     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfArray2seq.proof 
591175     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 202.6ns 
591176     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
593593     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.42s 
593593     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfArray2seq 
594396     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfArray2seq 
594399     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.15ms 
594401     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getAnyOfArray2seq.proof 
594401     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 54.7ns 
594401     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
596814     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.41s 
596814     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getAnyOfArray2seq 
597617     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getAnyOfArray2seq 
597621     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.99ms 
597622     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfArray2seq.proof 
597622     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 69.6ns 
597623     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
600020     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.4s 
600020     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfArray2seq 
600822     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfArray2seq 
600828     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.68ms 
600829     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_getAnyOfNPermInv.proof 
600829     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 64ns 
600830     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
603248     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.42s 
603249     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getAnyOfNPermInv 
604050     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getAnyOfNPermInv 
604056     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.29ms 
604058     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqNPermRange.proof 
604058     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 72.1ns 
604059     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
606466     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.41s 
606466     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqNPermRange 
607268     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqNPermRange 
607336     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 62.54ms 
607338     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermTrans.proof 
607338     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 77.9ns 
607339     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
609757     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.42s 
609757     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermTrans 
610576     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermTrans 
610602     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 23.53ms 
610604     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermRefl.proof 
610604     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 84.3ns 
610604     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
613009     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.41s 
613010     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermRefl 
613813     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermRefl 
613834     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 19.52ms 
613836     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermSplit.proof 
613836     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 72.4ns 
613836     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
616247     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.41s 
616247     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermSplit 
617053     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermSplit 
617056     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 373.11ns 
617058     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqNPermRight.proof 
617058     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 196.5ns 
617059     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
619471     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.41s 
619471     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqNPermRight 
620272     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqNPermRight 
620472     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 190.37ms 
620475     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermFromSwap.proof 
620475     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 220.1ns 
620476     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
622894     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.42s 
622895     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermFromSwap 
623701     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermFromSwap 
623751     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 45.86ms 
623752     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermTransAlt0.proof 
623752     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 74.2ns 
623753     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
626156     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.4s 
626157     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermTransAlt0 
626960     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermTransAlt0 
626962     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 373.01ns 
626964     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermTransAlt1.proof 
626964     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 90ns 
626965     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
629376     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.41s 
629376     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermTransAlt1 
630158     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermTransAlt1 
630160     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 363.81ns 
630161     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermTransAlt2.proof 
630161     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 68.8ns 
630162     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
632560     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.4s 
632560     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermTransAlt2 
633364     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermTransAlt2 
633366     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 361.41ns 
633368     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermTransAlt3.proof 
633368     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 56.5ns 
633368     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
635766     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.4s 
635766     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermTransAlt3 
636567     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermTransAlt3 
636569     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 497.41ns 
636570     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermForall.proof 
636570     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 64.3ns 
636571     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
638978     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.41s 
638979     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermForall 
639782     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermForall 
639870     INFO  Test worker     d.u.i.k.s.SMTFocusResults Analyzing unsat core: (L_1 L_3 L_4) 
639883     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 99.57ms 
639885     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermExists.proof 
639886     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 90.8ns 
639887     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
642313     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.43s 
642313     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermExists 
643115     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermExists 
643172     INFO  Test worker     d.u.i.k.s.SMTFocusResults Analyzing unsat core: (L_1 L_3 L_5 L_6 L_7) 
643173     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 55.77ms 
643174     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm2/Taclet_schiffl_lemma_2.proof 
643174     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 83.5ns 
643176     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
645603     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.43s 
645603     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: schiffl_lemma_2 
646410     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: schiffl_lemma_2 
646412     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3ns 
646438     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 1: 'macro split-prop' 
646482     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 2: 'rule allRight' 
646508     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 3: 'rule allRight' 
646516     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 4: 'macro split-prop' 
646526     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 5: 'rule 'seqPermDefLeft'' 
646529     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 6: 'rule 'andLeft'' 
646530     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 7: 'rule 'exLeft'' 
646534     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 8: 'macro split-prop' 
646551     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 9: 'rule  seqNPermRange' 
646553     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 10: 'instantiate var=iv with='v_x_0' occ=1' 
646567     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 11: 'rule impLeft' 
646569     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 12: 'tryclose branch' 
646788     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 13: 'rule andLeft' 
646790     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 14: 'rule andLeft' 
646791     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 15: 'instantiate var=iv with='v_y_0' occ=1' 
646792     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 16: 'rule impLeft' 
646793     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 17: 'tryclose branch' 
646909     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 18: 'rule andLeft' 
646910     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 19: 'rule andLeft' 
646913     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 20: 'rule seqNPermDefLeft' 
646915     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 21: 'instantiate var=iv with='v_x_0' occ=2' 
646917     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 22: 'rule impLeft' 
646917     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 23: 'tryclose branch' 
647061     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 24: 'rule exLeft' 
647064     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 25: 'rule andLeft' 
647065     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 26: 'rule andLeft' 
647066     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 27: 'instantiate hide var=iv with='v_y_0' occ=2' 
647068     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 28: 'rule impLeft' 
647071     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 29: 'tryclose branch' 
647191     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 30: 'rule exLeft' 
647192     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 31: 'rule andLeft' 
647193     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 32: 'rule andLeft' 
647194     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 33: 'instantiate var=iv with='jv_0' occ=1' 
647195     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 34: 'rule impLeft' 
647195     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 35: 'tryclose branch' 
647202     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 36: 'rule andLeft' 
647203     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 37: 'rule andLeft' 
647203     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 38: 'rule castAdd formula='s_0[jv_0] = v_x_0' occ=0' 
647205     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 39: 'instantiate hide var=iv with='jv_1' occ=1' 
647208     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 40: 'rule impLeft' 
647208     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 41: 'tryclose branch' 
647219     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 42: 'rule andLeft' 
647219     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 43: 'rule andLeft' 
647220     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 44: 'rule castAdd formula='s_0[jv_1] = v_y_0' occ=0' 
647221     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 45: 'instantiate var=iv  with='v_x_0'' 
647223     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 46: 'rule impLeft' 
647223     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 47: 'tryclose branch' 
647384     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 48: 'instantiate var=iv  with='v_y_0'' 
647385     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 49: 'rule impLeft' 
647386     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 50: 'tryclose branch' 
647517     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 51: 'cut 'v_x_0 = v_y_0'' 
647519     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)'' 
647521     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 53: 'rule andRight' 
647522     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 54: 'rule andRight' 
647523     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 55: 'rule andRight' 
647524     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 56: 'rule andRight' 
647525     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 57: 'rule lenOfSwap' 
647527     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 58: 'tryclose branch' 
647530     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 59: 'rule seqNPermSwapNPerm' 
647532     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 60: 'instantiate hide var='iv' with='v_x_0' occ=1' 
647533     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 61: 'instantiate hide var='jv' with='jv_0'' 
647533     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 62: 'rule impLeft' 
647534     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 63: 'tryclose branch' 
647632     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 64: 'tryclose branch' 
647635     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 65: 'rule allRight' 
647637     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 66: 'rule impRight' 
647638     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 67: 'rule andLeft' 
647639     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 68: 'instantiate var=iv with='v_iv_0'' 
647640     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 69: 'rule impLeft' 
647642     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 70: 'tryclose branch' 
647756     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 71: 'rule getOfSwap' 
647757     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 72: 'rule ifthenelse_negated' 
647758     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 73: 'rule ifthenelse_split occ=0' 
647760     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 74: 'rule andLeft' 
647761     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 75: 'rule andLeft' 
647761     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 76: 'rule andLeft' 
647763     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 77: 'rule ifthenelse_split occ=0' 
647764     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 78: 'tryclose branch' 
647848     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 79: 'rule ifthenelse_split occ=0' 
647849     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 80: 'tryclose branch' 
647934     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 81: 'tryclose branch' 
647938     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 82: 'tryclose branch' 
647943     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 83: 'rule getOfSwap' 
647945     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 84: 'rule ifthenelse_negated' 
647947     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 85: 'rule ifthenelse_split occ=0' 
647949     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 86: 'rule andLeft' 
647950     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 87: 'rule andLeft' 
647950     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 88: 'rule andLeft' 
647951     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 89: 'rule ifthenelse_split occ=0' 
647952     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 90: 'tryclose branch' 
647961     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 91: 'tryclose branch' 
647965     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 92: 'tryclose branch' 
648058     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 93: 'rule getOfSwap' 
648059     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 94: 'rule ifthenelse_negated' 
648061     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 95: 'rule ifthenelse_split occ=0' 
648063     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 96: 'rule andLeft' 
648063     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 97: 'rule andLeft' 
648064     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 98: 'rule andLeft' 
648064     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 99: 'rule ifthenelse_split occ=0' 
648067     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 100: 'tryclose branch' 
648117     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 101: 'tryclose branch' 
648122     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 102: 'tryclose branch' 
648209     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 103: 'cut '(int)s_0[v_x_0] = (int)s_0[v_y_0]'' 
648211     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 104: 'rule seqNPermInjective' 
648213     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 105: 'instantiate hide var=iv with='v_x_0'' 
648215     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 106: 'instantiate hide var=jv with='v_y_0'' 
648215     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 107: 'rule impLeft' 
648216     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 108: 'tryclose branch' 
648339     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 109: 'tryclose branch' 
648342     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 110: 'cut '(int)s_0[v_x_0] = v_x_0'' 
648343     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)'' 
648345     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 112: 'rule andRight' 
648346     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 113: 'rule andRight' 
648347     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 114: 'rule andRight' 
648348     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 115: 'rule andRight' 
648348     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 116: 'tryclose branch' 
648356     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 117: 'rule seqNPermSwapNPerm' 
648358     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 118: 'instantiate hide var=iv with='v_y_0'' 
648359     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 119: 'instantiate hide var=jv with='jv_1'' 
648360     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 120: 'tryclose branch' 
648445     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 121: 'rule allRight' 
648446     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 122: 'rule impRight' 
648447     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 123: 'rule andLeft' 
648448     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 124: 'instantiate var=iv with='v_iv_0'' 
648449     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 125: 'rule impLeft' 
648450     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 126: 'tryclose branch' 
648547     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 127: 'rule getOfSwap' 
648549     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 128: 'rule ifthenelse_negated' 
648550     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 129: 'rule ifthenelse_split occ=0' 
648551     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 130: 'rule andLeft' 
648552     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 131: 'rule andLeft' 
648552     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 132: 'rule andLeft' 
648553     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 133: 'rule ifthenelse_split occ=0' 
648554     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 134: 'tryclose branch' 
648633     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 135: 'rule ifthenelse_split occ=0' 
648635     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 136: 'tryclose branch' 
648708     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 137: 'instantiate var=iv with='v_y_0'' 
648709     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 138: 'rule impLeft' 
648710     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 139: 'tryclose branch' 
648714     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 140: 'tryclose branch' 
648718     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 141: 'tryclose branch' 
648722     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 142: 'tryclose branch' 
648841     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 143: 'rule getOfSwap' 
648842     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 144: 'rule ifthenelse_negated' 
648843     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 145: 'rule ifthenelse_split occ=0' 
648844     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 146: 'tryclose branch' 
648853     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 147: 'tryclose branch' 
648983     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 148: 'tryclose branch' 
652389     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 149: 'cut  '(int)s_0[v_y_0] = v_y_0'' 
652391     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)'' 
652397     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 151: 'rule andRight' 
652398     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 152: 'rule andRight' 
652399     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 153: 'rule andRight' 
652400     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 154: 'rule andRight' 
652401     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 155: 'tryclose branch' 
652409     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 156: 'rule seqNPermSwapNPerm' 
652410     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 157: 'instantiate hide var=iv with='v_x_0'' 
652412     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 158: 'instantiate hide var=jv with='jv_0'' 
652413     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 159: 'rule impLeft' 
652414     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 160: 'tryclose branch' 
652507     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 161: 'tryclose branch' 
652511     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 162: 'rule allRight' 
652512     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 163: 'rule impRight' 
652513     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 164: 'rule andLeft' 
652514     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 165: 'instantiate var=iv with='v_iv_0'' 
652514     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 166: 'rule impLeft' 
652515     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 167: 'tryclose branch' 
652606     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 168: 'rule getOfSwap' 
652608     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 169: 'rule ifthenelse_negated' 
652609     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 170: 'rule ifthenelse_split occ=0' 
652610     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 171: 'rule andLeft' 
652611     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 172: 'rule andLeft' 
652612     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 173: 'rule andLeft' 
652612     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 174: 'rule ifthenelse_split occ=0' 
652613     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 175: 'tryclose branch' 
652685     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 176: 'rule ifthenelse_split occ=0' 
652686     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 177: 'tryclose branch' 
652759     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 178: 'tryclose branch' 
652763     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 179: 'tryclose branch' 
652767     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 180: 'rule getOfSwap' 
652768     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 181: 'rule ifthenelse_negated' 
652769     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 182: 'rule ifthenelse_split occ=0' 
652770     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 183: 'tryclose branch' 
652779     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 184: 'tryclose branch' 
652855     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 185: 'rule getOfSwap' 
652857     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 186: 'rule ifthenelse_negated' 
652857     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 187: 'rule ifthenelse_split occ=0' 
652858     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 188: 'tryclose branch' 
652927     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 189: 'tryclose branch' 
652936     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 190: 'cut '(int)s_0[v_x_0]=v_y_0'' 
652937     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)'' 
652939     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 192: 'rule andRight' 
652940     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 193: 'rule andRight' 
652941     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 194: 'rule andRight' 
652942     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 195: 'rule andRight' 
652942     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 196: 'tryclose branch' 
652953     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 197: 'rule seqNPermSwapNPerm' 
652954     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 198: 'instantiate hide var=iv with='jv_0'' 
652955     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 199: 'instantiate hide var=jv with='v_x_0'' 
652956     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 200: 'rule impLeft' 
652957     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 201: 'tryclose branch' 
653041     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 202: 'rule seqNPermSwapNPerm formula='seqNPerm(seqSwap(s_0, jv_0, v_x_0))'' 
653043     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 203: 'instantiate hide var=iv with='jv_0'' 
653044     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 204: 'instantiate hide var=jv with='v_y_0'' 
653045     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 205: 'rule impLeft' 
653046     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 206: 'tryclose branch' 
653133     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 207: 'tryclose branch' 
653194     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 208: 'rule allRight' 
653195     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 209: 'rule impRight' 
653196     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 210: 'rule andLeft' 
653197     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 211: 'instantiate var=iv with='v_iv_0'' 
653198     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 212: 'rule impLeft' 
653198     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 213: 'tryclose branch' 
653291     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 214: 'rule getOfSwap' 
653292     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 215: 'rule ifthenelse_negated' 
653293     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 216: 'rule ifthenelse_split occ=0' 
653294     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 217: 'rule andLeft' 
653295     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 218: 'rule andLeft' 
653295     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 219: 'rule andLeft' 
653295     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 220: 'rule ifthenelse_split occ=0' 
653296     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 221: 'rule getOfSwap' 
653297     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 222: 'rule ifthenelse_negated' 
653298     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 223: 'rule ifthenelse_split occ=0' 
653299     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 224: 'rule andLeft' 
653299     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 225: 'rule andLeft' 
653300     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 226: 'rule andLeft' 
653300     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 227: 'rule ifthenelse_split occ=0' 
653301     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 228: 'tryclose branch' 
653382     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 229: 'rule ifthenelse_split occ=0' 
653383     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 230: 'tryclose branch' 
653389     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 231: 'tryclose branch' 
653461     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 232: 'tryclose branch' 
653536     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 233: 'rule ifthenelse_split' 
653537     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 234: 'rule getOfSwap' 
653538     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 235: 'rule ifthenelse_negated' 
653539     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 236: 'rule ifthenelse_split occ=0' 
653540     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 237: 'rule andLeft' 
653540     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 238: 'rule andLeft' 
653540     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 239: 'rule andLeft' 
653541     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 240: 'rule ifthenelse_split occ=0' 
653542     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 241: 'tryclose branch' 
653622     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 242: 'tryclose branch' 
653628     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 243: 'tryclose branch' 
653711     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 244: 'rule getOfSwap' 
653712     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 245: 'rule ifthenelse_negated' 
653712     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 246: 'rule ifthenelse_split occ=0' 
653713     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 247: 'rule andLeft' 
653714     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 248: 'rule andLeft' 
653714     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 249: 'rule andLeft' 
653714     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 250: 'rule ifthenelse_split occ=0' 
653715     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 251: 'tryclose branch' 
653720     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 252: 'rule ifthenelse_split occ=0' 
653720     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 253: 'tryclose branch' 
653794     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 254: 'tryclose branch' 
653799     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 255: 'tryclose branch' 
653804     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 256: 'tryclose branch' 
653897     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 257: 'rule getOfSwap' 
653899     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 258: 'rule ifthenelse_negated' 
653899     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 259: 'rule ifthenelse_split occ=0' 
653900     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 260: 'rule andLeft' 
653901     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 261: 'rule andLeft' 
653901     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 262: 'rule andLeft' 
653901     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 263: 'rule ifthenelse_split occ=0' 
653902     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 264: 'tryclose branch' 
653953     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 265: 'rule ifthenelse_split occ=0' 
653954     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 266: 'rule getOfSwap' 
653955     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 267: 'rule ifthenelse_negated' 
653955     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 268: 'rule ifthenelse_split occ=0' 
653956     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 269: 'tryclose branch' 
653961     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 270: 'tryclose branch' 
653966     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 271: 'tryclose branch' 
654077     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 272: 'tryclose branch' 
654166     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 273: 'rule getOfSwap' 
654167     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 274: 'rule ifthenelse_negated' 
654168     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 275: 'rule ifthenelse_split occ=0' 
654169     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 276: 'tryclose branch' 
654331     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 277: 'tryclose branch' 
654414     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 278: 'cut 'int::seqGet(s_0, v_y_0)=v_x_0'' 
654415     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 279: 'tryclose branch' 
657259     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 280: 'rule seqNPermSwapNPerm' 
657264     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 281: 'instantiate hide var=iv with='jv_1'' 
657266     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 282: 'instantiate hide var=jv with='v_y_0'' 
657267     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 283: 'rule impLeft' 
657267     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 284: 'tryclose branch' 
657376     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 285: 'rule seqNPermSwapNPerm formula='seqNPerm(seqSwap(s_0,jv_1,v_y_0))'' 
657378     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 286: 'instantiate hide var=iv with='jv_1'' 
657379     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 287: 'instantiate hide var=jv with='v_x_0'' 
657380     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 288: 'rule impLeft' 
657381     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 289: 'tryclose branch' 
657481     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 290: 'tryclose branch' 
660303     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 291: 'tryclose branch' 
663269     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 292: 'rule seqNPermSwapNPerm formula='seqNPerm(s_0)'' 
663274     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 293: 'instantiate hide var=iv with='v_x_0'' 
663275     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 294: 'instantiate hide var=jv with='jv_0'' 
663275     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 295: 'rule impLeft' 
663276     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 296: 'tryclose branch' 
663384     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 297: 'rule seqNPermSwapNPerm formula='seqNPerm(seqSwap(s_0,v_x_0,jv_0))'' 
663386     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 298: 'instantiate hide var=iv with='v_y_0'' 
663387     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 299: 'instantiate hide var=jv with='jv_1'' 
663388     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)' ...' 
663389     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 301: 'tryclose branch' 
664482     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm2/Taclet_schiffl_thm_1.proof 
664482     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 107.1ns 
664483     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
666975     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.49s 
666975     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: schiffl_thm_1 
667810     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: schiffl_thm_1 
667811     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 7.2ns 
667811     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 1: 'macro split-prop' 
667826     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 2: 'rule schiffl_lemma_2 formula='seqPerm(f_s, f_t)'' 
667839     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 3: 'instantiate hide var=x with='f_x'' 
667843     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 4: 'instantiate hide var=y with='f_y'' 
667845     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 5: 'rule impLeft' 
667846     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 6: 'tryclose branch' 
667851     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 7: 'rule exLeft' 
667853     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 8: 'macro split-prop' 
667856     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 9: 'rule seqPermDef occ=1' 
667859     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 10: 'rule andRight' 
667860     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 11: 'tryclose branch' 
667871     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 12: 'instantiate hide var=s with='r_0'' 
667873     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 13: 'rule andRight' 
667874     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 14: 'tryclose branch' 
667931     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 15: 'rule allRight' 
667933     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 16: 'rule impRight' 
667933     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 17: 'instantiate hide var=iv with='iv_0'' 
667934     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 18: 'rule impLeft' 
667935     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 19: 'tryclose branch' 
668010     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 20: 'rule andLeft' 
668011     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 21: 'rule seqNPermRange' 
668012     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 22: 'instantiate hide var=iv with='iv_0'' 
668014     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 23: 'rule impLeft' 
668015     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 24: 'tryclose branch' 
668019     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 25: 'rule andLeft' 
668019     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 26: 'rule andLeft' 
668020     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 27: 'rule seqNPermRange' 
668021     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 28: 'instantiate hide var=iv with='f_x'' 
668022     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 29: 'rule impLeft' 
668022     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 30: 'tryclose branch' 
668107     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 31: 'rule andLeft' 
668108     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 32: 'rule andLeft' 
668108     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 33: 'rule seqNPermRange' 
668109     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 34: 'instantiate hide var=iv with='f_y'' 
668110     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 35: 'rule impLeft' 
668111     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 36: 'tryclose branch' 
668202     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 37: 'rule andLeft' 
668203     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 38: 'rule andLeft' 
668203     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 39: 'rule getOfSeqDef occ=0' 
668204     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 40: 'rule getOfSeqDef' 
668205     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 41: 'rule ifthenelse_split occ=0' 
668205     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 42: 'rule andLeft occ=0' 
668206     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 43: 'rule sub_zero_2 occ=0' 
668206     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 44: 'rule ifthenelse_split occ=2' 
668207     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 45: 'rule andLeft' 
668207     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 46: 'rule sub_zero_2 occ=0' 
668207     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 47: 'rule add_zero_right occ=0' 
668208     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 48: 'rule add_zero_right occ=0' 
668208     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 49: 'rule add_zero_right occ=0' 
668209     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 50: 'rule add_zero_right occ=0' 
668209     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 51: 'rule add_zero_right occ=0' 
668209     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 52: 'rule add_zero_right occ=0' 
668210     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 53: 'rule ifthenelse_split occ=0' 
668211     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 54: 'rule ifthenelse_split occ=0' 
668211     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 55: 'tryclose branch' 
668214     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 56: 'tryclose branch' 
668255     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 57: 'rule ifthenelse_split occ=0' 
668256     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 58: 'tryclose branch' 
668321     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 59: 'rule ifthenelse_split occ=0' 
668322     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 60: 'rule seqNPermInjective' 
668323     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 61: 'instantiate hide var=iv with='iv_0'' 
668325     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 62: 'instantiate hide var=jv with='f_y'' 
668325     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 63: 'rule impLeft' 
668326     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 64: 'tryclose branch' 
668379     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 65: 'tryclose branch' 
668382     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 66: 'rule ifthenelse_split occ=0' 
668383     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 67: 'rule seqNPermInjective' 
668384     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 68: 'instantiate hide var=iv with='iv_0'' 
668385     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 69: 'instantiate hide var=jv with='f_x'' 
668386     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 70: 'rule impLeft' 
668386     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 71: 'tryclose branch' 
668440     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 72: 'tryclose branch' 
668442     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 73: 'tryclose branch' 
668445     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 74: 'tryclose branch' 
668504     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 75: 'tryclose branch' 
668555     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_eqSameSeq.proof 
668555     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 93.3ns 
668556     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
671029     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.47s 
671029     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: eqSameSeq 
671870     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: eqSameSeq 
671902     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 28.92ms