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

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

tests
0

failures
0

ignored
14m24.61s

duration
100%

successful

Tests

Test Method name Duration Result
powPositive data()[100] 4.049s passed
powPositiveConcrete data()[101] 4.153s passed
powGeq1Concrete data()[102] 4.231s passed
pow2InIntLower data()[103] 4.093s passed
pow2InIntUpper data()[104] 4.134s passed
logSelfConcrete data()[105] 4.179s passed
log1Concrete data()[106] 4.097s passed
logProduct data()[107] 4.110s passed
logTimesBaseConcrete data()[108] 4.134s passed
logProdIdentity data()[109] 4.211s passed
moduloByteIsInByte data()[10] 4.163s passed
logProdIdentityConcrete data()[110] 4.242s passed
logPowIdentity data()[111] 4.132s passed
logPowIdentityConcrete data()[112] 4.314s passed
logPositive data()[113] 4.299s passed
logPositiveConcrete data()[114] 4.172s passed
logMono data()[115] 4.186s passed
logMonoConcrete data()[116] 4.140s passed
powLogLess data()[117] 4.227s passed
powLogMore2 data()[118] 4.266s passed
logLessThanPow data()[119] 4.348s passed
moduloCharIsInChar data()[11] 4.221s passed
logLessThanPowConcrete data()[120] 4.263s passed
logSqueeze data()[121] 4.099s passed
ifthenelse_equals data()[122] 4.197s passed
ifthenelse_equals_1 data()[123] 4.246s passed
ifthenelse_equals_2 data()[124] 4.194s passed
disjointWithSingleton1 data()[125] 4.113s passed
disjointWithSingleton2 data()[126] 4.202s passed
disjointArrayRanges data()[127] 4.176s passed
disjointArrayRangeAllFields1 data()[128] 4.202s passed
disjointArrayRangeAllFields2 data()[129] 4.232s passed
div_unique1 data()[12] 4.219s passed
seqSelfDefinition data()[130] 4.263s passed
seqOutsideValue data()[131] 4.187s passed
castedGetAny data()[132] 4.238s passed
seqGetAlphaCast data()[133] 4.258s passed
getOfSeqSingleton data()[134] 4.319s passed
getOfSeqSingletonConcrete data()[135] 4.313s passed
getOfSeqConcat data()[136] 4.314s passed
getOfSeqSub data()[137] 4.311s passed
getOfSeqReverse data()[138] 4.289s passed
lenOfSeqEmpty data()[139] 4.198s passed
div_unique2 data()[13] 4.271s passed
lenOfSeqSingleton data()[140] 4.193s passed
lenOfSeqConcat data()[141] 4.276s passed
lenOfSeqSub data()[142] 4.291s passed
lenOfSeqReverse data()[143] 4.224s passed
equalityToSeqGetAndSeqLenLeft data()[144] 4.131s passed
equalityToSeqGetAndSeqLenRight data()[145] 4.214s passed
getOfSeqSingletonEQ data()[146] 4.198s passed
getOfSeqConcatEQ data()[147] 4.192s passed
getOfSeqSubEQ data()[148] 4.213s passed
getOfSeqReverseEQ data()[149] 4.214s passed
div_exists data()[14] 4.503s passed
lenOfSeqEmptyEQ data()[150] 4.184s passed
lenOfSeqSingletonEQ data()[151] 4.236s passed
lenOfSeqConcatEQ data()[152] 4.253s passed
lenOfSeqSubEQ data()[153] 4.214s passed
lenOfSeqReverseEQ data()[154] 4.172s passed
getOfSeqDefEQ data()[155] 4.235s passed
lenOfSeqDefEQ data()[156] 4.223s passed
seqConcatWithSeqEmpty1 data()[157] 4.141s passed
seqConcatWithSeqEmpty2 data()[158] 4.165s passed
seqReverseOfSeqEmpty data()[159] 4.209s passed
div_one data()[15] 4.271s passed
subSeqComplete data()[160] 4.255s passed
subSeqTailR data()[161] 4.214s passed
subSeqTailL data()[162] 4.504s passed
subSeqTailEQR data()[163] 4.338s passed
subSeqTailEQL data()[164] 4.251s passed
seqDef_split data()[165] 4.239s passed
seqDef_induction_upper data()[166] 4.309s passed
seqDef_induction_upper_concrete data()[167] 4.247s passed
seqDef_induction_lower data()[168] 4.227s passed
seqDef_induction_lower_concrete data()[169] 4.189s passed
jdiv_one data()[16] 4.102s passed
seqDef_split_in_three data()[170] 4.329s passed
seqDef_empty data()[171] 4.213s passed
seqDef_one_summand data()[172] 4.232s passed
seqDef_lower_equals_upper data()[173] 4.177s passed
seqDefOfSeq data()[174] 4.119s passed
seqSelfDefinitionEQ2 data()[175] 4.274s passed
indexOfSeqSingleton data()[176] 4.182s passed
indexOfSeqConcatFirst data()[177] 4.223s passed
indexOfSeqConcatSecond data()[178] 4.141s passed
indexOfSeqSub data()[179] 4.266s passed
div_zero data()[17] 4.333s passed
lenOfArray2seq data()[180] 4.314s passed
getAnyOfArray2seq data()[181] 4.171s passed
getOfArray2seq data()[182] 4.145s passed
getAnyOfNPermInv data()[183] 4.072s passed
seqNPermRange data()[184] 4.267s passed
seqPermTrans data()[185] 4.267s passed
seqPermRefl data()[186] 4.193s passed
seqPermSplit data()[187] 4.209s passed
seqNPermRight data()[188] 4.522s passed
seqPermFromSwap data()[189] 4.250s passed
divResZero1 data()[18] 4.306s passed
seqPermTransAlt0 data()[190] 4.125s passed
seqPermTransAlt1 data()[191] 4.199s passed
seqPermTransAlt2 data()[192] 4.182s passed
seqPermTransAlt3 data()[193] 4.212s passed
seqPermForall data()[194] 4.441s passed
seqPermExists data()[195] 4.351s passed
schiffl_lemma_2 data()[196] 31.810s passed
schiffl_thm_1 data()[197] 5.336s passed
eqSameSeq data()[198] 4.256s passed
divResZero2 data()[19] 4.364s passed
eqTermCut data()[1] 5.132s passed
divResOne1 data()[20] 4.424s passed
divResOne2 data()[21] 4.409s passed
div_cancel1 data()[22] 4.249s passed
div_cancel2 data()[23] 4.188s passed
divAddMultDenom data()[24] 4.212s passed
divMinus data()[25] 4.251s passed
divMinusDenom data()[26] 4.125s passed
divLeastDPos data()[27] 4.184s passed
divLeastDNeg data()[28] 4.183s passed
divGreatestDPos data()[29] 4.148s passed
equivAllRight data()[2] 4.859s passed
divGreatestDNeg data()[30] 4.198s passed
divIncreasingPos data()[31] 4.117s passed
divIncreasingNeg data()[32] 4.275s passed
jdiv_zero data()[33] 4.149s passed
jdivPulloutMinusNum data()[34] 4.092s passed
jdivPulloutMinusDenom data()[35] 4.173s passed
jdiv_uniquePosPos data()[36] 4.277s passed
jdiv_uniquePosNeg data()[37] 4.219s passed
jdiv_uniqueNegPos data()[38] 4.072s passed
jdiv_uniqueNegNeg data()[39] 4.133s passed
irrflConcrete1 data()[3] 4.622s passed
jdivMultDenom1 data()[40] 4.229s passed
jdivMultDenom2 data()[41] 4.091s passed
mod_geZero data()[42] 4.123s passed
mod_lessDenom data()[43] 4.067s passed
jmod_NumPos data()[44] 4.163s passed
jmod_NumNeg data()[45] 4.191s passed
jmod_geZero data()[46] 4.210s passed
jmodNumZero data()[47] 4.217s passed
jmod_pulloutminusNum data()[48] 4.158s passed
jmod_pulloutminusDenom data()[49] 4.083s passed
irrflConcrete2 data()[4] 4.446s passed
jmodUnique1 data()[50] 4.234s passed
jmodUnique2 data()[51] 4.410s passed
intDivRem data()[52] 4.221s passed
jmodjmod data()[53] 4.117s passed
jmodDivisible data()[54] 4.198s passed
jmodDivisibleRep data()[55] 4.097s passed
jdivAddMultDenom data()[56] 4.365s passed
jmodAltZero data()[57] 4.177s passed
jmodAddMultDenomZero data()[58] 4.116s passed
polyDiv_zero data()[59] 4.096s passed
cancel_gtPos data()[5] 4.311s passed
polyMod_ltdivDenom data()[60] 4.117s passed
bsum_empty data()[61] 4.154s passed
bsum_induction_upper data()[62] 4.100s passed
bsum_induction_lower data()[63] 4.227s passed
bsum_num_of_bounds data()[64] 4.147s passed
bsum_num_of_bounds2 data()[65] 4.280s passed
bsum_induction_upper2 data()[66] 4.187s passed
bsum_induction_upper_concrete data()[67] 4.069s passed
bsum_induction_upper_concrete_2 data()[68] 4.051s passed
bsum_induction_upper2_concrete data()[69] 4.163s passed
cancel_gtNeg data()[6] 4.337s passed
bsum_induction_lower_concrete data()[70] 4.039s passed
bsum_induction_lower2 data()[71] 4.048s passed
bsum_induction_lower2_concrete data()[72] 4.027s passed
bsum_positive data()[73] 4.233s passed
bsum_upper_bound data()[74] 4.300s passed
bsum_lower_bound data()[75] 4.205s passed
bsum_positive_lower_bound_element data()[76] 4.233s passed
bsum_sub_same_index data()[77] 4.155s passed
bsum_less_same_index data()[78] 4.236s passed
bsum_equal_except_one_index data()[79] 4.181s passed
moduloIntIsInInt data()[7] 4.276s passed
bsum_num_of_is_max data()[80] 4.175s passed
bsum_num_of_is_max2 data()[81] 4.226s passed
bsum_num_of_is_max3 data()[82] 4.150s passed
bsum_num_of_is_max4 data()[83] 4.044s passed
bsum_num_of_lt_max data()[84] 4.113s passed
bsum_num_of_lt_max2 data()[85] 4.224s passed
bsum_num_of_lt_max3 data()[86] 4.204s passed
bsum_num_of_lt_max4 data()[87] 4.187s passed
bsum_num_of_gt0 data()[88] 4.286s passed
bsum_num_of_gt0_alt data()[89] 4.192s passed
moduloLongIsInLong data()[8] 4.255s passed
bsum_add_concrete data()[90] 4.157s passed
bprod_all_positive data()[91] 4.485s passed
bprod_split data()[92] 4.306s passed
powConcrete0 data()[93] 4.218s passed
powConcrete1 data()[94] 4.223s passed
powSplitFactor data()[95] 4.140s passed
powAdd data()[96] 4.101s passed
powMono data()[97] 4.170s passed
powMonoConcrete data()[98] 4.095s passed
powMonoConcreteRight data()[99] 4.086s passed
moduloShortIsInShort data()[9] 4.284s passed

Standard output

480        INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src/test/resources/testcase/dummyTrue.key 
513        DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 13.8ms 
846        INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
875        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)

2201       DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for Meta 
2204       DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for Meta 
2208       DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for Meta 
2208       DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for Meta 
4487       DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for JavaBigintExpression 
11542      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 10.7s 
11663      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof dummyTrue.key 
11712      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 42.4ns 
11730      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/firstOrder/Taclet_eqTermCut.proof 
11731      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 475ns 
11736      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
15516      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.78s 
15520      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: eqTermCut 
16805      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: eqTermCut 
16850      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 29.16ms 
16864      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/firstOrder/Taclet_equivAllRight.proof 
16865      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 336.5ns 
16867      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
20555      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.69s 
20556      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: equivAllRight 
21704      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: equivAllRight 
21722      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 14.04ms 
21724      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_irrflConcrete1.proof 
21724      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 157.1ns 
21726      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
25233      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.51s 
25233      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: irrflConcrete1 
26335      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: irrflConcrete1 
26343      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.3ms 
26346      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_irrflConcrete2.proof 
26347      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 390.2ns 
26348      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
29695      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.35s 
29696      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: irrflConcrete2 
30782      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: irrflConcrete2 
30791      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.44ms 
30794      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_cancel_gtPos.proof 
30795      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 517.6ns 
30797      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
33984      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.19s 
33985      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: cancel_gtPos 
35044      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: cancel_gtPos 
35102      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 53.29ms 
35108      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_cancel_gtNeg.proof 
35108      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 481.3ns 
35110      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
38363      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.25s 
38364      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: cancel_gtNeg 
39393      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: cancel_gtNeg 
39441      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 44.3ms 
39445      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intRulesIgnoringOF/Taclet_moduloIntIsInInt.proof 
39446      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 371.1ns 
39447      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
42668      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.22s 
42669      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: moduloIntIsInInt 
43714      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: moduloIntIsInInt 
43718      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 932.8ns 
43721      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intRulesIgnoringOF/Taclet_moduloLongIsInLong.proof 
43721      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 248.1ns 
43723      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
46918      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.2s 
46919      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: moduloLongIsInLong 
47970      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: moduloLongIsInLong 
47974      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 787.4ns 
47977      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intRulesIgnoringOF/Taclet_moduloShortIsInShort.proof 
47977      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 405.8ns 
47979      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
51211      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.23s 
51212      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: moduloShortIsInShort 
52256      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: moduloShortIsInShort 
52259      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 684.61ns 
52262      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intRulesIgnoringOF/Taclet_moduloByteIsInByte.proof 
52263      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 567.4ns 
52267      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
55402      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.14s 
55403      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: moduloByteIsInByte 
56419      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: moduloByteIsInByte 
56422      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 786.61ns 
56424      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intRulesIgnoringOF/Taclet_moduloCharIsInChar.proof 
56425      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 394.6ns 
56426      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
59596      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.17s 
59597      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: moduloCharIsInChar 
60637      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: moduloCharIsInChar 
60641      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 801.51ns 
60645      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_div_unique1.proof 
60646      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 407.6ns 
60647      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
63781      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.13s 
63781      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: div_unique1 
64764      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: div_unique1 
64860      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 90.85ms 
64868      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_div_unique2.proof 
64868      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 255.9ns 
64869      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
68046      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.18s 
68046      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: div_unique2 
69063      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: div_unique2 
69135      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 68.59ms 
69138      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_div_exists.proof 
69138      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 128.9ns 
69141      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
72404      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.26s 
72405      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: div_exists 
73378      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: div_exists 
73638      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 249.87ms 
73643      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_div_one.proof 
73644      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 588.21ns 
73646      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
76830      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.18s 
76831      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: div_one 
77905      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: div_one 
77911      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.94ms 
77914      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdiv_one.proof 
77914      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 412ns 
77915      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
80985      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.07s 
80986      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdiv_one 
82010      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdiv_one 
82013      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.33ms 
82016      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_div_zero.proof 
82017      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 122.5ns 
82018      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
85237      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.22s 
85237      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: div_zero 
86278      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: div_zero 
86345      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 61.88ms 
86349      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divResZero1.proof 
86349      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 116.1ns 
86350      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
89615      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.26s 
89615      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divResZero1 
90630      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divResZero1 
90653      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 19.4ms 
90659      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divResZero2.proof 
90659      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 216.1ns 
90660      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
93944      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.28s 
93944      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divResZero2 
94997      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divResZero2 
95020      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 19.76ms 
95025      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divResOne1.proof 
95026      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 494.8ns 
95027      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
98306      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.28s 
98306      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divResOne1 
99409      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divResOne1 
99445      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 30.89ms 
99447      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divResOne2.proof 
99447      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 136.2ns 
99448      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
102784     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.34s 
102785     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divResOne2 
103828     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divResOne2 
103853     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 21.02ms 
103856     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_div_cancel1.proof 
103857     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 447ns 
103858     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
107027     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.17s 
107028     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: div_cancel1 
108062     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: div_cancel1 
108102     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 35.42ms 
108105     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_div_cancel2.proof 
108106     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 438.9ns 
108107     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
111289     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.18s 
111289     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: div_cancel2 
112287     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: div_cancel2 
112291     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.76ms 
112293     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divAddMultDenom.proof 
112293     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 101.5ns 
112294     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
115424     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.13s 
115425     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divAddMultDenom 
116440     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divAddMultDenom 
116502     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 56.74ms 
116504     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divMinus.proof 
116504     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 112.4ns 
116506     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
119649     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.14s 
119649     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divMinus 
120662     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divMinus 
120753     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 83.22ms 
120757     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divMinusDenom.proof 
120757     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 312.1ns 
120758     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
123833     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.07s 
123833     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divMinusDenom 
124809     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divMinusDenom 
124879     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 64.2ms 
124882     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divLeastDPos.proof 
124883     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 342.6ns 
124884     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
128025     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.14s 
128027     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divLeastDPos 
129045     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divLeastDPos 
129064     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 16.74ms 
129066     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divLeastDNeg.proof 
129066     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 122.9ns 
129067     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
132213     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.15s 
132213     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divLeastDNeg 
133223     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divLeastDNeg 
133244     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 18.07ms 
133249     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divGreatestDPos.proof 
133249     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 148.5ns 
133250     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
136433     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.18s 
136433     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divGreatestDPos 
137376     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divGreatestDPos 
137394     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 14.54ms 
137397     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divGreatestDNeg.proof 
137397     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 86.4ns 
137398     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
140543     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.14s 
140543     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divGreatestDNeg 
141566     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divGreatestDNeg 
141593     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 22.57ms 
141596     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divIncreasingPos.proof 
141596     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 335.2ns 
141598     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
144683     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.09s 
144683     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divIncreasingPos 
145697     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divIncreasingPos 
145709     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 9.17ms 
145712     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divIncreasingNeg.proof 
145713     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 419.4ns 
145714     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
148996     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.28s 
148997     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divIncreasingNeg 
149973     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divIncreasingNeg 
149985     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 8.54ms 
149988     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdiv_zero.proof 
149988     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 343.9ns 
149989     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
153135     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.15s 
153135     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdiv_zero 
154129     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdiv_zero 
154134     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.51ms 
154135     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdivPulloutMinusNum.proof 
154136     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 103.5ns 
154136     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
157193     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.06s 
157194     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdivPulloutMinusNum 
158188     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdivPulloutMinusNum 
158226     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 32.25ms 
158228     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdivPulloutMinusDenom.proof 
158229     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 222.5ns 
158234     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
161302     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.07s 
161303     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdivPulloutMinusDenom 
162285     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdivPulloutMinusDenom 
162397     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 106.52ms 
162402     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdiv_uniquePosPos.proof 
162402     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 338.5ns 
162405     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
165610     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.21s 
165611     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdiv_uniquePosPos 
166617     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdiv_uniquePosPos 
166674     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 53.47ms 
166679     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdiv_uniquePosNeg.proof 
166679     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 327.4ns 
166681     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
169853     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.17s 
169853     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdiv_uniquePosNeg 
170865     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdiv_uniquePosNeg 
170896     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 26.8ms 
170898     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdiv_uniqueNegPos.proof 
170898     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 118.3ns 
170899     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
173962     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.06s 
173962     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdiv_uniqueNegPos 
174939     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdiv_uniqueNegPos 
174968     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 25.56ms 
174970     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdiv_uniqueNegNeg.proof 
174970     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 97.2ns 
174972     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
178058     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.09s 
178059     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdiv_uniqueNegNeg 
179075     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdiv_uniqueNegNeg 
179102     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 23.15ms 
179103     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdivMultDenom1.proof 
179103     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 87.7ns 
179104     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
182239     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.13s 
182240     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdivMultDenom1 
183263     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdivMultDenom1 
183329     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 58.89ms 
183332     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdivMultDenom2.proof 
183332     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 346.6ns 
183333     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
186447     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.11s 
186448     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdivMultDenom2 
187416     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdivMultDenom2 
187421     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.14ms 
187423     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_mod_geZero.proof 
187423     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 187ns 
187424     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
190557     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.13s 
190557     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: mod_geZero 
191539     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: mod_geZero 
191545     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.55ms 
191546     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_mod_lessDenom.proof 
191546     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 112.2ns 
191547     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
194592     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.04s 
194593     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: mod_lessDenom 
195597     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: mod_lessDenom 
195611     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 11.3ms 
195613     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmod_NumPos.proof 
195613     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 101.1ns 
195614     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
198737     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.12s 
198737     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmod_NumPos 
199762     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmod_NumPos 
199774     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 9.61ms 
199776     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmod_NumNeg.proof 
199776     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 88.7ns 
199777     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
202900     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.12s 
202900     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmod_NumNeg 
203936     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmod_NumNeg 
203966     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 25.75ms 
203967     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmod_geZero.proof 
203968     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 103.8ns 
203969     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
207160     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.19s 
207160     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmod_geZero 
208163     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmod_geZero 
208175     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 9.17ms 
208177     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmodNumZero.proof 
208177     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 80.6ns 
208178     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
211334     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.16s 
211334     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmodNumZero 
212388     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmodNumZero 
212392     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.9ms 
212400     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmod_pulloutminusNum.proof 
212406     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 5.43ms 
212407     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
215532     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.12s 
215533     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmod_pulloutminusNum 
216548     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmod_pulloutminusNum 
216555     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.53ms 
216557     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmod_pulloutminusDenom.proof 
216558     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 280.9ns 
216559     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
219644     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.09s 
219644     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmod_pulloutminusDenom 
220632     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmod_pulloutminusDenom 
220639     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.72ms 
220640     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmodUnique1.proof 
220640     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 80.6ns 
220641     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
223719     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.08s 
223719     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmodUnique1 
224744     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmodUnique1 
224872     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 117.53ms 
224875     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmodUnique2.proof 
224875     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 280.8ns 
224877     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
228138     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.26s 
228139     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmodUnique2 
229139     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmodUnique2 
229281     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 128.56ms 
229284     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_intDivRem.proof 
229285     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 307.2ns 
229286     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
232460     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.17s 
232462     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: intDivRem 
233498     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: intDivRem 
233503     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.56ms 
233515     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmodjmod.proof 
233515     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 300.9ns 
233516     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
236567     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.05s 
236567     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmodjmod 
237576     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmodjmod 
237630     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 50.23ms 
237632     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmodDivisible.proof 
237632     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 247.4ns 
237633     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
240749     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.12s 
240750     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmodDivisible 
241778     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmodDivisible 
241828     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 42.45ms 
241830     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmodDivisibleRep.proof 
241830     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 85.5ns 
241830     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
244869     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.04s 
244869     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmodDivisibleRep 
245921     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmodDivisibleRep 
245925     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.66ms 
245927     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdivAddMultDenom.proof 
245927     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 73.9ns 
245929     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
249051     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.12s 
249052     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdivAddMultDenom 
250032     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdivAddMultDenom 
250289     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 245.43ms 
250292     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmodAltZero.proof 
250294     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 1.31ms 
250295     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
253447     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.15s 
253447     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmodAltZero 
254450     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmodAltZero 
254467     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 14.42ms 
254469     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmodAddMultDenomZero.proof 
254469     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 82.4ns 
254470     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
257577     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.11s 
257577     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmodAddMultDenomZero 
258562     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmodAddMultDenomZero 
258583     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 14.97ms 
258585     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_polyDiv_zero.proof 
258585     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 227.7ns 
258587     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
261667     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.08s 
261667     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: polyDiv_zero 
262652     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: polyDiv_zero 
262679     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 23.84ms 
262681     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_polyMod_ltdivDenom.proof 
262681     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 85.5ns 
262682     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
265775     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.09s 
265775     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: polyMod_ltdivDenom 
266774     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: polyMod_ltdivDenom 
266795     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 11.26ms 
266799     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_empty.proof 
266799     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 326.4ns 
266800     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
269942     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.14s 
269943     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_empty 
270944     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_empty 
270949     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.31ms 
270951     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_induction_upper.proof 
270952     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 83.9ns 
270952     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
274055     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.1s 
274055     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_upper 
275044     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_induction_upper 
275050     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.07ms 
275052     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_induction_lower.proof 
275052     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 76.8ns 
275053     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
278252     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.2s 
278252     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_lower 
279242     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_induction_lower 
279277     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 32.37ms 
279279     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_bounds.proof 
279279     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 69.9ns 
279280     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
282369     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.09s 
282369     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_bounds 
283393     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_bounds 
283423     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 25.94ms 
283427     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_bounds2.proof 
283429     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 1.42ms 
283434     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
286604     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.17s 
286604     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_bounds2 
287675     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_bounds2 
287704     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 25.6ms 
287708     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_induction_upper2.proof 
287708     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 284.7ns 
287709     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
290872     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.16s 
290872     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_upper2 
291882     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_induction_upper2 
291892     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 7.06ms 
291894     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_induction_upper_concrete.proof 
291894     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 267.3ns 
291896     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
294961     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.07s 
294961     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_upper_concrete 
295955     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_induction_upper_concrete 
295961     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.56ms 
295963     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_induction_upper_concrete_2.proof 
295963     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 121.6ns 
295964     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
299026     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.06s 
299026     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_upper_concrete_2 
300004     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_induction_upper_concrete_2 
300012     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 6.19ms 
300013     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_induction_upper2_concrete.proof 
300014     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 84.8ns 
300014     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
303139     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.12s 
303139     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_upper2_concrete 
304170     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_induction_upper2_concrete 
304175     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.31ms 
304177     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_induction_lower_concrete.proof 
304178     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 162.5ns 
304179     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
307221     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.04s 
307222     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_lower_concrete 
308211     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_induction_lower_concrete 
308214     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.08ms 
308216     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_induction_lower2.proof 
308216     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 66.8ns 
308217     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
311281     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.06s 
311282     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_lower2 
312257     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_induction_lower2 
312262     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.6ms 
312264     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_induction_lower2_concrete.proof 
312264     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 79.4ns 
312265     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
315327     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.06s 
315327     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_lower2_concrete 
316286     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_induction_lower2_concrete 
316289     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.45ms 
316291     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_positive.proof 
316291     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 111.3ns 
316292     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
319433     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.14s 
319433     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_positive 
320454     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_positive 
320522     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 65.11ms 
320524     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_upper_bound.proof 
320525     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 276.4ns 
320526     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
323728     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.2s 
323728     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_upper_bound 
324764     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_upper_bound 
324822     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 54.93ms 
324824     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_lower_bound.proof 
324824     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 81.6ns 
324829     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
327996     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.17s 
327996     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_lower_bound 
328971     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_lower_bound 
329027     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 52.92ms 
329029     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_positive_lower_bound_element.proof 
329029     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 80.9ns 
329030     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
332199     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.17s 
332200     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_positive_lower_bound_element 
333173     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_positive_lower_bound_element 
333259     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 80.76ms 
333262     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_sub_same_index.proof 
333262     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 206.9ns 
333263     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
336366     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.1s 
336366     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_sub_same_index 
337364     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_sub_same_index 
337416     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 48.31ms 
337417     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_less_same_index.proof 
337417     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 84.6ns 
337418     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
340609     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.19s 
340610     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_less_same_index 
341564     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_less_same_index 
341651     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 81.11ms 
341653     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_equal_except_one_index.proof 
341654     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 220.1ns 
341655     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
344732     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.08s 
344732     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_equal_except_one_index 
345780     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_equal_except_one_index 
345832     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 47.82ms 
345834     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_is_max.proof 
345834     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 89.5ns 
345836     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
348972     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.14s 
348972     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_is_max 
349974     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_is_max 
350008     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 30.34ms 
350009     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_is_max2.proof 
350009     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 91.1ns 
350010     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
353168     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.16s 
353169     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_is_max2 
354181     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_is_max2 
354233     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 47.58ms 
354236     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_is_max3.proof 
354236     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 249ns 
354237     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
357351     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.11s 
357351     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_is_max3 
358353     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_is_max3 
358384     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 28.12ms 
358386     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_is_max4.proof 
358386     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 77ns 
358387     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
361386     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3s 
361387     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_is_max4 
362381     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_is_max4 
362428     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 44.1ms 
362430     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_lt_max.proof 
362430     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 84.9ns 
362431     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
365516     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.09s 
365516     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_lt_max 
366497     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_lt_max 
366540     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 39.9ms 
366542     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_lt_max2.proof 
366543     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 112.6ns 
366543     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
369707     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.16s 
369707     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_lt_max2 
370708     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_lt_max2 
370764     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 50.47ms 
370768     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_lt_max3.proof 
370768     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 204.4ns 
370769     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
373895     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.13s 
373896     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_lt_max3 
374927     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_lt_max3 
374969     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 37.87ms 
374970     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_lt_max4.proof 
374970     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 92.6ns 
374972     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
378112     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.14s 
378112     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_lt_max4 
379119     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_lt_max4 
379156     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 32.54ms 
379158     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_gt0.proof 
379158     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 95.4ns 
379159     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
382372     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.21s 
382372     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_gt0 
383397     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_gt0 
383442     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 41.21ms 
383444     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_gt0_alt.proof 
383444     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 84.5ns 
383445     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
386558     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.11s 
386558     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_gt0_alt 
387590     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_gt0_alt 
387633     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 39.56ms 
387636     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_add_concrete.proof 
387636     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 270.7ns 
387637     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
390805     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.17s 
390805     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_add_concrete 
391780     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_add_concrete 
391791     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 8.77ms 
391793     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bprod/Taclet_bprod_all_positive.proof 
391793     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 73.2ns 
391794     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
395171     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.38s 
395171     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bprod_all_positive 
396243     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bprod_all_positive 
396276     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 29.65ms 
396278     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bprod/Taclet_bprod_split.proof 
396278     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 69.9ns 
396279     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
399551     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.27s 
399552     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bprod_split 
400569     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bprod_split 
400582     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 10.74ms 
400584     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powConcrete0.proof 
400584     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 79.2ns 
400585     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
403766     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.18s 
403766     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powConcrete0 
404795     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powConcrete0 
404800     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.13ms 
404802     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powConcrete1.proof 
404802     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 79.6ns 
404803     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
408020     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.22s 
408021     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powConcrete1 
409020     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powConcrete1 
409023     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.22ms 
409025     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powSplitFactor.proof 
409025     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 67.7ns 
409026     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
412142     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.12s 
412142     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powSplitFactor 
413150     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powSplitFactor 
413163     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 8.95ms 
413164     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powAdd.proof 
413165     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 136.8ns 
413165     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
416275     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.11s 
416275     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powAdd 
417255     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powAdd 
417265     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 7.15ms 
417266     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powMono.proof 
417266     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 92.1ns 
417267     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
420400     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.13s 
420400     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powMono 
421414     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powMono 
421434     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 17.61ms 
421436     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powMonoConcrete.proof 
421436     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 79.6ns 
421437     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
424524     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.09s 
424524     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powMonoConcrete 
425524     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powMonoConcrete 
425529     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.39ms 
425530     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powMonoConcreteRight.proof 
425531     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 65.1ns 
425532     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
428635     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.1s 
428635     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powMonoConcreteRight 
429613     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powMonoConcreteRight 
429616     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 841.51ns 
429617     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powPositive.proof 
429617     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 62.8ns 
429618     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
432669     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.05s 
432669     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powPositive 
433656     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powPositive 
433664     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 5.42ms 
433665     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powPositiveConcrete.proof 
433666     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 67ns 
433666     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
436816     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.15s 
436816     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powPositiveConcrete 
437814     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powPositiveConcrete 
437817     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.18ms 
437819     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powGeq1Concrete.proof 
437819     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 70.3ns 
437820     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
441065     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.25s 
441065     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powGeq1Concrete 
442046     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powGeq1Concrete 
442048     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 922.91ns 
442050     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_pow2InIntLower.proof 
442050     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 76.9ns 
442051     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
445151     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.1s 
445152     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: pow2InIntLower 
446138     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: pow2InIntLower 
446141     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 898.41ns 
446143     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_pow2InIntUpper.proof 
446143     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 91.6ns 
446144     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
449238     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.09s 
449238     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: pow2InIntUpper 
450270     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: pow2InIntUpper 
450276     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.33ms 
450277     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logSelfConcrete.proof 
450277     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 81.7ns 
450278     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
453426     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.15s 
453426     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logSelfConcrete 
454440     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logSelfConcrete 
454454     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 11.42ms 
454456     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_log1Concrete.proof 
454456     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 84ns 
454457     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
457560     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.1s 
457560     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: log1Concrete 
458543     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: log1Concrete 
458551     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.3ms 
458553     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logProduct.proof 
458553     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 217.5ns 
458559     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
461626     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.07s 
461626     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logProduct 
462650     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logProduct 
462661     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 8.14ms 
462663     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logTimesBaseConcrete.proof 
462663     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 63.5ns 
462664     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
465740     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.08s 
465740     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logTimesBaseConcrete 
466788     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logTimesBaseConcrete 
466795     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.43ms 
466796     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logProdIdentity.proof 
466796     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 75.5ns 
466797     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
469956     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.16s 
469956     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logProdIdentity 
470981     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logProdIdentity 
471005     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 20.53ms 
471008     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logProdIdentityConcrete.proof 
471008     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 212.8ns 
471009     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
474165     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.16s 
474165     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logProdIdentityConcrete 
475242     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logProdIdentityConcrete 
475248     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.14ms 
475250     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logPowIdentity.proof 
475250     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 76.7ns 
475250     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
478372     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.12s 
478373     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logPowIdentity 
479375     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logPowIdentity 
479380     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.14ms 
479382     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logPowIdentityConcrete.proof 
479382     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 90.8ns 
479382     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
482610     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.23s 
482611     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logPowIdentityConcrete 
483689     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logPowIdentityConcrete 
483694     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.32ms 
483696     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logPositive.proof 
483696     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 62.5ns 
483697     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
486943     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.25s 
486944     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logPositive 
487965     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logPositive 
487993     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 24.18ms 
487995     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logPositiveConcrete.proof 
487995     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 111.7ns 
487996     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
491172     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.18s 
491172     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logPositiveConcrete 
492158     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logPositiveConcrete 
492164     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 812.71ns 
492167     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logMono.proof 
492167     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 60.5ns 
492168     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
495301     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.13s 
495301     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logMono 
496292     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logMono 
496351     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 53.91ms 
496353     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logMonoConcrete.proof 
496353     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 90.7ns 
496354     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
499460     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.11s 
499461     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logMonoConcrete 
500484     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logMonoConcrete 
500491     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.68ms 
500492     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powLogLess.proof 
500492     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 61.2ns 
500495     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
503682     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.19s 
503683     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powLogLess 
504676     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powLogLess 
504718     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 33.37ms 
504721     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powLogMore2.proof 
504721     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 105ns 
504722     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
507869     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.15s 
507869     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powLogMore2 
508944     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powLogMore2 
508984     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 36.56ms 
508986     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logLessThanPow.proof 
508986     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 75.9ns 
508987     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
512264     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.28s 
512264     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logLessThanPow 
513291     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logLessThanPow 
513332     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 37.09ms 
513334     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logLessThanPowConcrete.proof 
513334     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 92.9ns 
513335     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
516565     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.23s 
516565     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logLessThanPowConcrete 
517592     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logLessThanPowConcrete 
517595     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 837.61ns 
517596     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logSqueeze.proof 
517597     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 60.5ns 
517597     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
520710     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.11s 
520710     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logSqueeze 
521687     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logSqueeze 
521695     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 5.39ms 
521696     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/booleanRules/Taclet_ifthenelse_equals.proof 
521696     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 103.4ns 
521697     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
524841     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.14s 
524841     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: ifthenelse_equals 
525886     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: ifthenelse_equals 
525891     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.53ms 
525892     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/booleanRules/Taclet_ifthenelse_equals_1.proof 
525893     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 76.8ns 
525893     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
529105     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.21s 
529105     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: ifthenelse_equals_1 
530133     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: ifthenelse_equals_1 
530137     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.18ms 
530138     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/booleanRules/Taclet_ifthenelse_equals_2.proof 
530138     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 59.9ns 
530139     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
533311     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.17s 
533311     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: ifthenelse_equals_2 
534328     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: ifthenelse_equals_2 
534331     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.23ms 
534332     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/locSet/Taclet_disjointWithSingleton1.proof 
534333     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 109.7ns 
534333     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
537408     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.07s 
537408     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: disjointWithSingleton1 
538439     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: disjointWithSingleton1 
538445     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.68ms 
538446     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/locSet/Taclet_disjointWithSingleton2.proof 
538446     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 68.7ns 
538447     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
541597     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.15s 
541597     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: disjointWithSingleton2 
542642     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: disjointWithSingleton2 
542646     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.98ms 
542648     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/locSet/Taclet_disjointArrayRanges.proof 
542648     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 67.6ns 
542649     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
545781     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.13s 
545782     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: disjointArrayRanges 
546807     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: disjointArrayRanges 
546822     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 11.78ms 
546824     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/locSet/Taclet_disjointArrayRangeAllFields1.proof 
546824     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 62ns 
546825     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
549969     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.14s 
549969     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: disjointArrayRangeAllFields1 
551005     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: disjointArrayRangeAllFields1 
551024     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 17.11ms 
551026     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/locSet/Taclet_disjointArrayRangeAllFields2.proof 
551026     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 111.6ns 
551027     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
554246     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.22s 
554246     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: disjointArrayRangeAllFields2 
555236     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: disjointArrayRangeAllFields2 
555256     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 15.94ms 
555259     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqSelfDefinition.proof 
555259     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 359.2ns 
555260     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
558472     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.21s 
558472     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqSelfDefinition 
559500     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqSelfDefinition 
559519     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 16.49ms 
559521     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqOutsideValue.proof 
559521     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 116.6ns 
559522     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
562681     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.16s 
562681     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqOutsideValue 
563700     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqOutsideValue 
563706     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.83ms 
563708     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_castedGetAny.proof 
563708     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 71.8ns 
563709     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
566895     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.19s 
566895     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: castedGetAny 
567935     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: castedGetAny 
567944     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 7.08ms 
567946     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqGetAlphaCast.proof 
567946     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 77.2ns 
567947     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
571148     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.2s 
571148     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqGetAlphaCast 
572199     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqGetAlphaCast 
572202     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.19ms 
572204     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqSingleton.proof 
572204     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 115.8ns 
572205     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
575485     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.28s 
575485     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqSingleton 
576517     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqSingleton 
576521     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.58ms 
576523     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqSingletonConcrete.proof 
576523     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 254.8ns 
576524     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
579766     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.24s 
579766     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqSingletonConcrete 
580831     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqSingletonConcrete 
580834     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.36ms 
580837     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqConcat.proof 
580837     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 228.7ns 
580838     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
584090     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.25s 
584091     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqConcat 
585129     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqConcat 
585149     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 17.41ms 
585151     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqSub.proof 
585151     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 83.8ns 
585152     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
588377     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.23s 
588377     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqSub 
589452     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqSub 
589460     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.97ms 
589461     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqReverse.proof 
589461     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 72.2ns 
589462     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
592681     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.22s 
592681     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqReverse 
593740     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqReverse 
593750     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 7.29ms 
593751     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqEmpty.proof 
593751     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 126.4ns 
593754     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
596937     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.18s 
596937     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqEmpty 
597944     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqEmpty 
597948     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.07ms 
597949     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqSingleton.proof 
597949     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 69.7ns 
597950     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
601086     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.14s 
601086     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqSingleton 
602137     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqSingleton 
602140     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 971.81ns 
602141     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqConcat.proof 
602141     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 74.3ns 
602142     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
605357     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.21s 
605357     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqConcat 
606410     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqConcat 
606416     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.63ms 
606417     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqSub.proof 
606418     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 135.4ns 
606418     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
609654     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.24s 
609655     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqSub 
610703     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqSub 
610707     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.56ms 
610709     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqReverse.proof 
610709     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 89.9ns 
610710     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
613902     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.19s 
613902     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqReverse 
614925     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqReverse 
614931     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.18ms 
614932     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_equalityToSeqGetAndSeqLenLeft.proof 
614933     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 60ns 
614933     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
618050     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.12s 
618050     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: equalityToSeqGetAndSeqLenLeft 
619059     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: equalityToSeqGetAndSeqLenLeft 
619063     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.7ms 
619064     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_equalityToSeqGetAndSeqLenRight.proof 
619064     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 142.7ns 
619065     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
622245     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.18s 
622245     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: equalityToSeqGetAndSeqLenRight 
623268     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: equalityToSeqGetAndSeqLenRight 
623276     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 5.32ms 
623278     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqSingletonEQ.proof 
623278     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 61.4ns 
623279     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
626403     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.12s 
626403     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqSingletonEQ 
627470     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqSingletonEQ 
627474     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.26ms 
627476     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqConcatEQ.proof 
627476     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 69.7ns 
627477     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
630621     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.14s 
630621     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqConcatEQ 
631649     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqConcatEQ 
631666     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 14.45ms 
631668     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqSubEQ.proof 
631668     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 80.4ns 
631669     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
634831     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.16s 
634832     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqSubEQ 
635876     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqSubEQ 
635880     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 951.71ns 
635881     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqReverseEQ.proof 
635881     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 71ns 
635882     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
639014     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.13s 
639014     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqReverseEQ 
640081     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqReverseEQ 
640093     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 9.23ms 
640094     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqEmptyEQ.proof 
640094     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 63.4ns 
640095     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
643202     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.11s 
643202     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqEmptyEQ 
644274     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqEmptyEQ 
644277     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.32ms 
644278     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqSingletonEQ.proof 
644279     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 59ns 
644279     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
647465     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.19s 
647465     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqSingletonEQ 
648510     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqSingletonEQ 
648513     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.11ms 
648515     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqConcatEQ.proof 
648515     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 73.8ns 
648516     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
651702     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.19s 
651703     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqConcatEQ 
652759     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqConcatEQ 
652766     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.65ms 
652767     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqSubEQ.proof 
652767     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 53.7ns 
652768     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
655957     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.19s 
655958     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqSubEQ 
656976     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqSubEQ 
656980     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.43ms 
656981     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqReverseEQ.proof 
656981     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 66.5ns 
656982     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
660105     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.12s 
660105     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqReverseEQ 
661147     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqReverseEQ 
661152     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.77ms 
661154     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqDefEQ.proof 
661154     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 75.6ns 
661155     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
664360     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.21s 
664360     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqDefEQ 
665382     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqDefEQ 
665387     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.19ms 
665391     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqDefEQ.proof 
665391     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 58.4ns 
665391     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
668562     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.17s 
668562     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqDefEQ 
669605     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqDefEQ 
669612     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.89ms 
669614     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqConcatWithSeqEmpty1.proof 
669614     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 66.4ns 
669615     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
672725     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.11s 
672725     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqConcatWithSeqEmpty1 
673732     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqConcatWithSeqEmpty1 
673753     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 18.87ms 
673755     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqConcatWithSeqEmpty2.proof 
673755     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 73.5ns 
673756     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
676883     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.13s 
676883     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqConcatWithSeqEmpty2 
677896     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqConcatWithSeqEmpty2 
677918     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 19.89ms 
677920     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqReverseOfSeqEmpty.proof 
677920     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 71.2ns 
677921     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
681087     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.17s 
681087     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqReverseOfSeqEmpty 
682112     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqReverseOfSeqEmpty 
682127     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 13.49ms 
682129     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_subSeqComplete.proof 
682129     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 82.7ns 
682130     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
685315     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.18s 
685315     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: subSeqComplete 
686366     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: subSeqComplete 
686382     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 14.07ms 
686384     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_subSeqTailR.proof 
686384     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 69ns 
686385     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
689501     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.12s 
689501     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: subSeqTailR 
690553     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: subSeqTailR 
690596     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 37.19ms 
690598     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_subSeqTailL.proof 
690599     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 65.7ns 
690599     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
693958     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.36s 
693958     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: subSeqTailL 
695061     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: subSeqTailL 
695100     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 36.02ms 
695102     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_subSeqTailEQR.proof 
695102     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 100.7ns 
695103     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
698341     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.24s 
698341     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: subSeqTailEQR 
699401     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: subSeqTailEQR 
699438     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 34.56ms 
699440     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_subSeqTailEQL.proof 
699440     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 55.3ns 
699441     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
702614     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.17s 
702614     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: subSeqTailEQL 
703667     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: subSeqTailEQL 
703689     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 18.97ms 
703691     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDef_split.proof 
703691     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 67.7ns 
703692     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
706859     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.17s 
706859     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_split 
707871     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDef_split 
707928     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 53.01ms 
707931     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDef_induction_upper.proof 
707931     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 219.8ns 
707932     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
711119     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.19s 
711119     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_induction_upper 
712163     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDef_induction_upper 
712238     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 70.79ms 
712240     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDef_induction_upper_concrete.proof 
712240     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 70.3ns 
712241     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
715372     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.13s 
715373     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_induction_upper_concrete 
716415     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDef_induction_upper_concrete 
716485     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 66.53ms 
716487     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDef_induction_lower.proof 
716487     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 70.3ns 
716488     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
719613     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.13s 
719614     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_induction_lower 
720648     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDef_induction_lower 
720712     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 58.99ms 
720713     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDef_induction_lower_concrete.proof 
720713     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 74.1ns 
720714     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
723800     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.09s 
723801     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_induction_lower_concrete 
724833     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDef_induction_lower_concrete 
724901     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 64.42ms 
724903     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDef_split_in_three.proof 
724903     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 71.5ns 
724904     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
728018     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.11s 
728018     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_split_in_three 
729051     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDef_split_in_three 
729230     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 171.16ms 
729232     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDef_empty.proof 
729232     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 73.1ns 
729233     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
732406     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.17s 
732406     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_empty 
733431     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDef_empty 
733443     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 9.01ms 
733445     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDef_one_summand.proof 
733445     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 59.3ns 
733446     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
736666     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.22s 
736667     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_one_summand 
737664     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDef_one_summand 
737676     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 9.04ms 
737677     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDef_lower_equals_upper.proof 
737677     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 55ns 
737678     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
740820     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.14s 
740820     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_lower_equals_upper 
741844     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDef_lower_equals_upper 
741852     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 5.54ms 
741854     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDefOfSeq.proof 
741854     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 69.3ns 
741854     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
744944     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.09s 
744944     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDefOfSeq 
745941     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDefOfSeq 
745971     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 26.3ms 
745973     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqSelfDefinitionEQ2.proof 
745973     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 69.3ns 
745974     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
749158     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.18s 
749158     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqSelfDefinitionEQ2 
750228     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqSelfDefinitionEQ2 
750245     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 14.5ms 
750247     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_indexOfSeqSingleton.proof 
750247     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 59.9ns 
750248     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
753380     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.13s 
753380     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: indexOfSeqSingleton 
754422     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: indexOfSeqSingleton 
754427     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.9ms 
754429     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_indexOfSeqConcatFirst.proof 
754429     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 88.2ns 
754429     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
757586     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.16s 
757586     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: indexOfSeqConcatFirst 
758624     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: indexOfSeqConcatFirst 
758650     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 23.42ms 
758651     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_indexOfSeqConcatSecond.proof 
758651     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 71.8ns 
758652     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
761751     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.1s 
761752     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: indexOfSeqConcatSecond 
762767     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: indexOfSeqConcatSecond 
762792     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 21.76ms 
762793     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_indexOfSeqSub.proof 
762793     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 70.2ns 
762794     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
765995     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.2s 
765995     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: indexOfSeqSub 
767027     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: indexOfSeqSub 
767057     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 27.53ms 
767062     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfArray2seq.proof 
767062     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 238ns 
767063     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
770290     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.23s 
770290     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfArray2seq 
771370     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfArray2seq 
771374     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.71ms 
771376     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getAnyOfArray2seq.proof 
771376     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 58.4ns 
771377     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
774515     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.14s 
774515     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getAnyOfArray2seq 
775537     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getAnyOfArray2seq 
775546     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 6.17ms 
775548     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfArray2seq.proof 
775548     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 227.8ns 
775549     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
778637     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.09s 
778638     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfArray2seq 
779681     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfArray2seq 
779690     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 7.15ms 
779692     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_getAnyOfNPermInv.proof 
779692     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 64.7ns 
779692     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
782739     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.05s 
782739     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getAnyOfNPermInv 
783751     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getAnyOfNPermInv 
783763     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 8.67ms 
783764     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqNPermRange.proof 
783764     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 71.6ns 
783765     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
786853     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.09s 
786853     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqNPermRange 
787914     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqNPermRange 
788028     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 106.99ms 
788031     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermTrans.proof 
788031     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 192.4ns 
788032     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
791217     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.19s 
791217     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermTrans 
792252     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermTrans 
792296     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 39.54ms 
792297     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermRefl.proof 
792297     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 60.3ns 
792298     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
795418     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.12s 
795418     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermRefl 
796456     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermRefl 
796489     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 30.47ms 
796491     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermSplit.proof 
796491     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 96.2ns 
796491     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
799615     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.12s 
799615     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermSplit 
800696     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermSplit 
800698     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 429.4ns 
800700     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqNPermRight.proof 
800700     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 60.3ns 
800701     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
803888     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.19s 
803889     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqNPermRight 
804916     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqNPermRight 
805219     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 290.3ms 
805222     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermFromSwap.proof 
805223     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 1.01ms 
805224     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
808373     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.15s 
808373     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermFromSwap 
809395     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermFromSwap 
809470     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 70.07ms 
809472     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermTransAlt0.proof 
809472     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 56.6ns 
809473     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
812571     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.1s 
812571     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermTransAlt0 
813592     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermTransAlt0 
813595     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 555.91ns 
813596     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermTransAlt1.proof 
813597     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 57.8ns 
813597     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
816750     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.15s 
816752     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermTransAlt1 
817792     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermTransAlt1 
817794     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 453.11ns 
817796     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermTransAlt2.proof 
817796     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 67.5ns 
817797     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
820950     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.15s 
820950     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermTransAlt2 
821974     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermTransAlt2 
821976     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 478.2ns 
821978     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermTransAlt3.proof 
821978     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 66.2ns 
821979     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
825132     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.15s 
825132     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermTransAlt3 
826186     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermTransAlt3 
826189     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 816.81ns 
826190     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermForall.proof 
826190     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 68.6ns 
826191     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
829433     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.24s 
829433     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermForall 
830475     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermForall 
830603     INFO  Test worker     d.u.i.k.s.SMTFocusResults Analyzing unsat core: (L_1 L_3 L_4) 
830628     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 149.46ms 
830633     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermExists.proof 
830633     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 320.5ns 
830634     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
833926     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.29s 
833926     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermExists 
834916     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermExists 
834981     INFO  Test worker     d.u.i.k.s.SMTFocusResults Analyzing unsat core: (L_1 L_3 L_5 L_6 L_7) 
834982     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 63.61ms 
834983     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm2/Taclet_schiffl_lemma_2.proof 
834984     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 71.8ns 
834985     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
838115     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.13s 
838115     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: schiffl_lemma_2 
839177     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: schiffl_lemma_2 
839179     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.5ns 
839216     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 1: 'macro split-prop' 
839272     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 2: 'rule allRight' 
839301     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 3: 'rule allRight' 
839311     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 4: 'macro split-prop' 
839321     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 5: 'rule 'seqPermDefLeft'' 
839324     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 6: 'rule 'andLeft'' 
839325     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 7: 'rule 'exLeft'' 
839329     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 8: 'macro split-prop' 
839334     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 9: 'rule  seqNPermRange' 
839336     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 10: 'instantiate var=iv with='v_x_0' occ=1' 
839344     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 11: 'rule impLeft' 
839346     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 12: 'tryclose branch' 
839638     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 13: 'rule andLeft' 
839640     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 14: 'rule andLeft' 
839642     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 15: 'instantiate var=iv with='v_y_0' occ=1' 
839644     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 16: 'rule impLeft' 
839645     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 17: 'tryclose branch' 
839823     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 18: 'rule andLeft' 
839825     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 19: 'rule andLeft' 
839828     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 20: 'rule seqNPermDefLeft' 
839831     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 21: 'instantiate var=iv with='v_x_0' occ=2' 
839832     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 22: 'rule impLeft' 
839833     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 23: 'tryclose branch' 
840128     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 24: 'rule exLeft' 
840130     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 25: 'rule andLeft' 
840132     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 26: 'rule andLeft' 
840132     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 27: 'instantiate hide var=iv with='v_y_0' occ=2' 
840134     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 28: 'rule impLeft' 
840137     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 29: 'tryclose branch' 
840336     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 30: 'rule exLeft' 
840338     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 31: 'rule andLeft' 
840339     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 32: 'rule andLeft' 
840340     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 33: 'instantiate var=iv with='jv_0' occ=1' 
840341     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 34: 'rule impLeft' 
840342     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 35: 'tryclose branch' 
840354     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 36: 'rule andLeft' 
840355     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 37: 'rule andLeft' 
840356     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 38: 'rule castAdd formula='s_0[jv_0] = v_x_0' occ=0' 
840359     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 39: 'instantiate hide var=iv with='jv_1' occ=1' 
840362     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 40: 'rule impLeft' 
840363     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 41: 'tryclose branch' 
840376     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 42: 'rule andLeft' 
840378     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 43: 'rule andLeft' 
840378     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 44: 'rule castAdd formula='s_0[jv_1] = v_y_0' occ=0' 
840382     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 45: 'instantiate var=iv  with='v_x_0'' 
840383     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 46: 'rule impLeft' 
840384     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 47: 'tryclose branch' 
840592     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 48: 'instantiate var=iv  with='v_y_0'' 
840593     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 49: 'rule impLeft' 
840596     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 50: 'tryclose branch' 
840775     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 51: 'cut 'v_x_0 = v_y_0'' 
840776     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)'' 
840780     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 53: 'rule andRight' 
840781     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 54: 'rule andRight' 
840782     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 55: 'rule andRight' 
840783     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 56: 'rule andRight' 
840785     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 57: 'rule lenOfSwap' 
840788     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 58: 'tryclose branch' 
840793     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 59: 'rule seqNPermSwapNPerm' 
840794     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 60: 'instantiate hide var='iv' with='v_x_0' occ=1' 
840795     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 61: 'instantiate hide var='jv' with='jv_0'' 
840796     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 62: 'rule impLeft' 
840797     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 63: 'tryclose branch' 
840966     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 64: 'tryclose branch' 
840971     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 65: 'rule allRight' 
840973     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 66: 'rule impRight' 
840974     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 67: 'rule andLeft' 
840975     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 68: 'instantiate var=iv with='v_iv_0'' 
840976     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 69: 'rule impLeft' 
840979     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 70: 'tryclose branch' 
841185     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 71: 'rule getOfSwap' 
841186     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 72: 'rule ifthenelse_negated' 
841187     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 73: 'rule ifthenelse_split occ=0' 
841190     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 74: 'rule andLeft' 
841191     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 75: 'rule andLeft' 
841192     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 76: 'rule andLeft' 
841193     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 77: 'rule ifthenelse_split occ=0' 
841195     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 78: 'tryclose branch' 
841368     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 79: 'rule ifthenelse_split occ=0' 
841370     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 80: 'tryclose branch' 
841497     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 81: 'tryclose branch' 
841503     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 82: 'tryclose branch' 
841511     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 83: 'rule getOfSwap' 
841512     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 84: 'rule ifthenelse_negated' 
841516     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 85: 'rule ifthenelse_split occ=0' 
841518     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 86: 'rule andLeft' 
841518     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 87: 'rule andLeft' 
841519     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 88: 'rule andLeft' 
841520     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 89: 'rule ifthenelse_split occ=0' 
841521     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 90: 'tryclose branch' 
841534     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 91: 'tryclose branch' 
841540     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 92: 'tryclose branch' 
841683     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 93: 'rule getOfSwap' 
841685     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 94: 'rule ifthenelse_negated' 
841688     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 95: 'rule ifthenelse_split occ=0' 
841690     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 96: 'rule andLeft' 
841691     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 97: 'rule andLeft' 
841691     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 98: 'rule andLeft' 
841692     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 99: 'rule ifthenelse_split occ=0' 
841694     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 100: 'tryclose branch' 
841771     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 101: 'tryclose branch' 
841779     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 102: 'tryclose branch' 
841945     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 103: 'cut '(int)s_0[v_x_0] = (int)s_0[v_y_0]'' 
841947     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 104: 'rule seqNPermInjective' 
841950     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 105: 'instantiate hide var=iv with='v_x_0'' 
841952     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 106: 'instantiate hide var=jv with='v_y_0'' 
841953     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 107: 'rule impLeft' 
841956     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 108: 'tryclose branch' 
842154     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 109: 'tryclose branch' 
842160     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 110: 'cut '(int)s_0[v_x_0] = v_x_0'' 
842163     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)'' 
842165     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 112: 'rule andRight' 
842166     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 113: 'rule andRight' 
842167     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 114: 'rule andRight' 
842169     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 115: 'rule andRight' 
842169     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 116: 'tryclose branch' 
842181     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 117: 'rule seqNPermSwapNPerm' 
842189     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 118: 'instantiate hide var=iv with='v_y_0'' 
842190     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 119: 'instantiate hide var=jv with='jv_1'' 
842191     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 120: 'tryclose branch' 
842331     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 121: 'rule allRight' 
842333     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 122: 'rule impRight' 
842335     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 123: 'rule andLeft' 
842337     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 124: 'instantiate var=iv with='v_iv_0'' 
842338     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 125: 'rule impLeft' 
842339     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 126: 'tryclose branch' 
842511     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 127: 'rule getOfSwap' 
842513     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 128: 'rule ifthenelse_negated' 
842514     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 129: 'rule ifthenelse_split occ=0' 
842516     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 130: 'rule andLeft' 
842517     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 131: 'rule andLeft' 
842517     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 132: 'rule andLeft' 
842518     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 133: 'rule ifthenelse_split occ=0' 
842519     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 134: 'tryclose branch' 
842642     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 135: 'rule ifthenelse_split occ=0' 
842644     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 136: 'tryclose branch' 
842755     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 137: 'instantiate var=iv with='v_y_0'' 
842756     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 138: 'rule impLeft' 
842757     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 139: 'tryclose branch' 
842765     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 140: 'tryclose branch' 
842774     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 141: 'tryclose branch' 
842780     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 142: 'tryclose branch' 
842952     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 143: 'rule getOfSwap' 
842954     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 144: 'rule ifthenelse_negated' 
842955     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 145: 'rule ifthenelse_split occ=0' 
842956     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 146: 'tryclose branch' 
842971     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 147: 'tryclose branch' 
843095     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 148: 'tryclose branch' 
848566     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 149: 'cut  '(int)s_0[v_y_0] = v_y_0'' 
848567     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)'' 
848577     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 151: 'rule andRight' 
848578     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 152: 'rule andRight' 
848579     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 153: 'rule andRight' 
848580     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 154: 'rule andRight' 
848582     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 155: 'tryclose branch' 
848594     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 156: 'rule seqNPermSwapNPerm' 
848596     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 157: 'instantiate hide var=iv with='v_x_0'' 
848597     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 158: 'instantiate hide var=jv with='jv_0'' 
848598     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 159: 'rule impLeft' 
848599     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 160: 'tryclose branch' 
848737     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 161: 'tryclose branch' 
848742     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 162: 'rule allRight' 
848744     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 163: 'rule impRight' 
848745     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 164: 'rule andLeft' 
848745     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 165: 'instantiate var=iv with='v_iv_0'' 
848746     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 166: 'rule impLeft' 
848747     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 167: 'tryclose branch' 
848883     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 168: 'rule getOfSwap' 
848885     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 169: 'rule ifthenelse_negated' 
848886     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 170: 'rule ifthenelse_split occ=0' 
848889     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 171: 'rule andLeft' 
848891     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 172: 'rule andLeft' 
848892     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 173: 'rule andLeft' 
848893     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 174: 'rule ifthenelse_split occ=0' 
848894     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 175: 'tryclose branch' 
849002     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 176: 'rule ifthenelse_split occ=0' 
849004     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 177: 'tryclose branch' 
849126     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 178: 'tryclose branch' 
849133     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 179: 'tryclose branch' 
849139     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 180: 'rule getOfSwap' 
849140     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 181: 'rule ifthenelse_negated' 
849141     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 182: 'rule ifthenelse_split occ=0' 
849142     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 183: 'tryclose branch' 
849158     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 184: 'tryclose branch' 
849338     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 185: 'rule getOfSwap' 
849340     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 186: 'rule ifthenelse_negated' 
849341     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 187: 'rule ifthenelse_split occ=0' 
849342     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 188: 'tryclose branch' 
849441     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 189: 'tryclose branch' 
849453     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 190: 'cut '(int)s_0[v_x_0]=v_y_0'' 
849454     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)'' 
849456     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 192: 'rule andRight' 
849457     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 193: 'rule andRight' 
849458     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 194: 'rule andRight' 
849458     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 195: 'rule andRight' 
849459     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 196: 'tryclose branch' 
849474     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 197: 'rule seqNPermSwapNPerm' 
849475     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 198: 'instantiate hide var=iv with='jv_0'' 
849477     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 199: 'instantiate hide var=jv with='v_x_0'' 
849478     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 200: 'rule impLeft' 
849478     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 201: 'tryclose branch' 
849599     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 202: 'rule seqNPermSwapNPerm formula='seqNPerm(seqSwap(s_0, jv_0, v_x_0))'' 
849601     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 203: 'instantiate hide var=iv with='jv_0'' 
849602     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 204: 'instantiate hide var=jv with='v_y_0'' 
849603     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 205: 'rule impLeft' 
849604     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 206: 'tryclose branch' 
849730     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 207: 'tryclose branch' 
849736     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 208: 'rule allRight' 
849737     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 209: 'rule impRight' 
849738     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 210: 'rule andLeft' 
849740     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 211: 'instantiate var=iv with='v_iv_0'' 
849741     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 212: 'rule impLeft' 
849741     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 213: 'tryclose branch' 
849880     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 214: 'rule getOfSwap' 
849882     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 215: 'rule ifthenelse_negated' 
849883     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 216: 'rule ifthenelse_split occ=0' 
849884     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 217: 'rule andLeft' 
849885     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 218: 'rule andLeft' 
849885     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 219: 'rule andLeft' 
849886     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 220: 'rule ifthenelse_split occ=0' 
849887     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 221: 'rule getOfSwap' 
849888     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 222: 'rule ifthenelse_negated' 
849889     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 223: 'rule ifthenelse_split occ=0' 
849890     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 224: 'rule andLeft' 
849891     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 225: 'rule andLeft' 
849891     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 226: 'rule andLeft' 
849892     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 227: 'rule ifthenelse_split occ=0' 
849893     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 228: 'tryclose branch' 
850017     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 229: 'rule ifthenelse_split occ=0' 
850018     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 230: 'tryclose branch' 
850026     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 231: 'tryclose branch' 
850137     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 232: 'tryclose branch' 
850251     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 233: 'rule ifthenelse_split' 
850253     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 234: 'rule getOfSwap' 
850254     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 235: 'rule ifthenelse_negated' 
850255     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 236: 'rule ifthenelse_split occ=0' 
850257     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 237: 'rule andLeft' 
850257     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 238: 'rule andLeft' 
850258     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 239: 'rule andLeft' 
850258     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 240: 'rule ifthenelse_split occ=0' 
850259     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 241: 'tryclose branch' 
850382     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 242: 'tryclose branch' 
850390     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 243: 'tryclose branch' 
850514     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 244: 'rule getOfSwap' 
850515     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 245: 'rule ifthenelse_negated' 
850516     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 246: 'rule ifthenelse_split occ=0' 
850518     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 247: 'rule andLeft' 
850518     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 248: 'rule andLeft' 
850518     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 249: 'rule andLeft' 
850519     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 250: 'rule ifthenelse_split occ=0' 
850520     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 251: 'tryclose branch' 
850527     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 252: 'rule ifthenelse_split occ=0' 
850528     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 253: 'tryclose branch' 
850636     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 254: 'tryclose branch' 
850643     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 255: 'tryclose branch' 
850650     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 256: 'tryclose branch' 
850784     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 257: 'rule getOfSwap' 
850785     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 258: 'rule ifthenelse_negated' 
850786     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 259: 'rule ifthenelse_split occ=0' 
850787     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 260: 'rule andLeft' 
850788     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 261: 'rule andLeft' 
850788     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 262: 'rule andLeft' 
850789     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 263: 'rule ifthenelse_split occ=0' 
850790     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 264: 'tryclose branch' 
850866     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 265: 'rule ifthenelse_split occ=0' 
850867     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 266: 'rule getOfSwap' 
850868     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 267: 'rule ifthenelse_negated' 
850869     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 268: 'rule ifthenelse_split occ=0' 
850870     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 269: 'tryclose branch' 
850877     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 270: 'tryclose branch' 
850884     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 271: 'tryclose branch' 
851041     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 272: 'tryclose branch' 
851172     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 273: 'rule getOfSwap' 
851173     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 274: 'rule ifthenelse_negated' 
851174     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 275: 'rule ifthenelse_split occ=0' 
851175     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 276: 'tryclose branch' 
851415     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 277: 'tryclose branch' 
851608     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 278: 'cut 'int::seqGet(s_0, v_y_0)=v_x_0'' 
851609     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 279: 'tryclose branch' 
855804     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 280: 'rule seqNPermSwapNPerm' 
855810     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 281: 'instantiate hide var=iv with='jv_1'' 
855811     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 282: 'instantiate hide var=jv with='v_y_0'' 
855812     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 283: 'rule impLeft' 
855812     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 284: 'tryclose branch' 
855968     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 285: 'rule seqNPermSwapNPerm formula='seqNPerm(seqSwap(s_0,jv_1,v_y_0))'' 
855970     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 286: 'instantiate hide var=iv with='jv_1'' 
855971     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 287: 'instantiate hide var=jv with='v_x_0'' 
855972     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 288: 'rule impLeft' 
855973     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 289: 'tryclose branch' 
856178     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 290: 'tryclose branch' 
860390     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 291: 'tryclose branch' 
864923     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 292: 'rule seqNPermSwapNPerm formula='seqNPerm(s_0)'' 
864929     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 293: 'instantiate hide var=iv with='v_x_0'' 
864930     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 294: 'instantiate hide var=jv with='jv_0'' 
864931     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 295: 'rule impLeft' 
864932     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 296: 'tryclose branch' 
865090     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 297: 'rule seqNPermSwapNPerm formula='seqNPerm(seqSwap(s_0,v_x_0,jv_0))'' 
865093     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 298: 'instantiate hide var=iv with='v_y_0'' 
865094     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 299: 'instantiate hide var=jv with='jv_1'' 
865096     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)' ...' 
865098     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 301: 'tryclose branch' 
866793     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm2/Taclet_schiffl_thm_1.proof 
866793     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 106.3ns 
866795     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
870242     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.45s 
870243     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: schiffl_thm_1 
871276     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: schiffl_thm_1 
871278     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 8.5ns 
871278     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 1: 'macro split-prop' 
871286     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 2: 'rule schiffl_lemma_2 formula='seqPerm(f_s, f_t)'' 
871302     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 3: 'instantiate hide var=x with='f_x'' 
871305     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 4: 'instantiate hide var=y with='f_y'' 
871307     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 5: 'rule impLeft' 
871308     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 6: 'tryclose branch' 
871313     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 7: 'rule exLeft' 
871316     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 8: 'macro split-prop' 
871319     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 9: 'rule seqPermDef occ=1' 
871323     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 10: 'rule andRight' 
871324     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 11: 'tryclose branch' 
871336     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 12: 'instantiate hide var=s with='r_0'' 
871338     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 13: 'rule andRight' 
871338     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 14: 'tryclose branch' 
871401     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 15: 'rule allRight' 
871402     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 16: 'rule impRight' 
871402     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 17: 'instantiate hide var=iv with='iv_0'' 
871403     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 18: 'rule impLeft' 
871404     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 19: 'tryclose branch' 
871482     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 20: 'rule andLeft' 
871482     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 21: 'rule seqNPermRange' 
871484     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 22: 'instantiate hide var=iv with='iv_0'' 
871485     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 23: 'rule impLeft' 
871486     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 24: 'tryclose branch' 
871490     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 25: 'rule andLeft' 
871490     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 26: 'rule andLeft' 
871491     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 27: 'rule seqNPermRange' 
871492     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 28: 'instantiate hide var=iv with='f_x'' 
871493     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 29: 'rule impLeft' 
871494     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 30: 'tryclose branch' 
871597     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 31: 'rule andLeft' 
871598     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 32: 'rule andLeft' 
871599     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 33: 'rule seqNPermRange' 
871600     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 34: 'instantiate hide var=iv with='f_y'' 
871601     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 35: 'rule impLeft' 
871602     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 36: 'tryclose branch' 
871708     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 37: 'rule andLeft' 
871709     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 38: 'rule andLeft' 
871709     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 39: 'rule getOfSeqDef occ=0' 
871710     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 40: 'rule getOfSeqDef' 
871711     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 41: 'rule ifthenelse_split occ=0' 
871712     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 42: 'rule andLeft occ=0' 
871713     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 43: 'rule sub_zero_2 occ=0' 
871713     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 44: 'rule ifthenelse_split occ=2' 
871714     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 45: 'rule andLeft' 
871715     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 46: 'rule sub_zero_2 occ=0' 
871715     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 47: 'rule add_zero_right occ=0' 
871715     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 48: 'rule add_zero_right occ=0' 
871716     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 49: 'rule add_zero_right occ=0' 
871717     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 50: 'rule add_zero_right occ=0' 
871717     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 51: 'rule add_zero_right occ=0' 
871718     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 52: 'rule add_zero_right occ=0' 
871718     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 53: 'rule ifthenelse_split occ=0' 
871720     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 54: 'rule ifthenelse_split occ=0' 
871721     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 55: 'tryclose branch' 
871725     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 56: 'tryclose branch' 
871773     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 57: 'rule ifthenelse_split occ=0' 
871774     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 58: 'tryclose branch' 
871840     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 59: 'rule ifthenelse_split occ=0' 
871841     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 60: 'rule seqNPermInjective' 
871843     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 61: 'instantiate hide var=iv with='iv_0'' 
871844     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 62: 'instantiate hide var=jv with='f_y'' 
871845     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 63: 'rule impLeft' 
871845     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 64: 'tryclose branch' 
871903     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 65: 'tryclose branch' 
871906     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 66: 'rule ifthenelse_split occ=0' 
871907     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 67: 'rule seqNPermInjective' 
871909     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 68: 'instantiate hide var=iv with='iv_0'' 
871911     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 69: 'instantiate hide var=jv with='f_x'' 
871911     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 70: 'rule impLeft' 
871912     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 71: 'tryclose branch' 
871972     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 72: 'tryclose branch' 
871975     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 73: 'tryclose branch' 
871979     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 74: 'tryclose branch' 
872051     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 75: 'tryclose branch' 
872129     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_eqSameSeq.proof 
872130     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 106.2ns 
872131     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
875237     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.11s 
875238     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: eqSameSeq 
876334     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: eqSameSeq 
876384     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 45.13ms