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

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

tests
0

failures
0

ignored
10m53.94s

duration
100%

successful

Tests

Test Method name Duration Result
powPositive data()[100] 3.151s passed
powPositiveConcrete data()[101] 3.173s passed
powGeq1Concrete data()[102] 3.159s passed
pow2InIntLower data()[103] 3.138s passed
pow2InIntUpper data()[104] 3.172s passed
logSelfConcrete data()[105] 3.154s passed
log1Concrete data()[106] 3.166s passed
logProduct data()[107] 3.148s passed
logTimesBaseConcrete data()[108] 3.132s passed
logProdIdentity data()[109] 3.176s passed
moduloByteIsInByte data()[10] 3.257s passed
logProdIdentityConcrete data()[110] 3.151s passed
logPowIdentity data()[111] 3.169s passed
logPowIdentityConcrete data()[112] 3.155s passed
logPositive data()[113] 3.188s passed
logPositiveConcrete data()[114] 3.156s passed
logMono data()[115] 3.183s passed
logMonoConcrete data()[116] 3.148s passed
powLogLess data()[117] 3.178s passed
powLogMore2 data()[118] 3.179s passed
logLessThanPow data()[119] 3.185s passed
moduloCharIsInChar data()[11] 3.217s passed
logLessThanPowConcrete data()[120] 3.148s passed
logSqueeze data()[121] 3.170s passed
ifthenelse_equals data()[122] 3.146s passed
ifthenelse_equals_1 data()[123] 3.177s passed
ifthenelse_equals_2 data()[124] 3.160s passed
disjointWithSingleton1 data()[125] 3.150s passed
disjointWithSingleton2 data()[126] 3.182s passed
disjointArrayRanges data()[127] 3.193s passed
disjointArrayRangeAllFields1 data()[128] 3.214s passed
disjointArrayRangeAllFields2 data()[129] 3.245s passed
div_unique1 data()[12] 3.388s passed
seqSelfDefinition data()[130] 3.168s passed
seqOutsideValue data()[131] 3.176s passed
castedGetAny data()[132] 3.175s passed
seqGetAlphaCast data()[133] 3.157s passed
getOfSeqSingleton data()[134] 3.174s passed
getOfSeqSingletonConcrete data()[135] 3.164s passed
getOfSeqConcat data()[136] 3.171s passed
getOfSeqSub data()[137] 3.210s passed
getOfSeqReverse data()[138] 3.183s passed
lenOfSeqEmpty data()[139] 3.167s passed
div_unique2 data()[13] 3.252s passed
lenOfSeqSingleton data()[140] 3.130s passed
lenOfSeqConcat data()[141] 3.173s passed
lenOfSeqSub data()[142] 3.159s passed
lenOfSeqReverse data()[143] 3.172s passed
equalityToSeqGetAndSeqLenLeft data()[144] 3.178s passed
equalityToSeqGetAndSeqLenRight data()[145] 3.158s passed
getOfSeqSingletonEQ data()[146] 3.162s passed
getOfSeqConcatEQ data()[147] 3.186s passed
getOfSeqSubEQ data()[148] 3.159s passed
getOfSeqReverseEQ data()[149] 3.155s passed
div_exists data()[14] 3.370s passed
lenOfSeqEmptyEQ data()[150] 3.157s passed
lenOfSeqSingletonEQ data()[151] 3.181s passed
lenOfSeqConcatEQ data()[152] 3.190s passed
lenOfSeqSubEQ data()[153] 3.181s passed
lenOfSeqReverseEQ data()[154] 3.157s passed
getOfSeqDefEQ data()[155] 3.155s passed
lenOfSeqDefEQ data()[156] 3.164s passed
seqConcatWithSeqEmpty1 data()[157] 3.173s passed
seqConcatWithSeqEmpty2 data()[158] 3.198s passed
seqReverseOfSeqEmpty data()[159] 3.198s passed
div_one data()[15] 3.280s passed
subSeqComplete data()[160] 3.196s passed
subSeqTailR data()[161] 3.199s passed
subSeqTailL data()[162] 3.194s passed
subSeqTailEQR data()[163] 3.190s passed
subSeqTailEQL data()[164] 3.191s passed
seqDef_split data()[165] 3.196s passed
seqDef_induction_upper data()[166] 3.234s passed
seqDef_induction_upper_concrete data()[167] 3.289s passed
seqDef_induction_lower data()[168] 3.205s passed
seqDef_induction_lower_concrete data()[169] 3.199s passed
jdiv_one data()[16] 3.226s passed
seqDef_split_in_three data()[170] 3.269s passed
seqDef_empty data()[171] 3.187s passed
seqDef_one_summand data()[172] 3.200s passed
seqDef_lower_equals_upper data()[173] 3.180s passed
seqDefOfSeq data()[174] 3.162s passed
seqSelfDefinitionEQ2 data()[175] 3.155s passed
indexOfSeqSingleton data()[176] 3.168s passed
indexOfSeqConcatFirst data()[177] 3.157s passed
indexOfSeqConcatSecond data()[178] 3.190s passed
indexOfSeqSub data()[179] 3.186s passed
div_zero data()[17] 3.214s passed
lenOfArray2seq data()[180] 3.165s passed
getAnyOfArray2seq data()[181] 3.164s passed
getOfArray2seq data()[182] 3.212s passed
getAnyOfNPermInv data()[183] 3.176s passed
seqNPermRange data()[184] 3.287s passed
seqPermTrans data()[185] 3.235s passed
seqPermRefl data()[186] 3.233s passed
seqPermSplit data()[187] 3.152s passed
seqNPermRight data()[188] 3.369s passed
seqPermFromSwap data()[189] 3.218s passed
divResZero1 data()[18] 3.243s passed
seqPermTransAlt0 data()[190] 3.175s passed
seqPermTransAlt1 data()[191] 3.223s passed
seqPermTransAlt2 data()[192] 3.291s passed
seqPermTransAlt3 data()[193] 3.215s passed
seqPermForall data()[194] 3.272s passed
seqPermExists data()[195] 3.243s passed
schiffl_lemma_2 data()[196] 21.966s passed
schiffl_thm_1 data()[197] 3.923s passed
eqSameSeq data()[198] 3.282s passed
divResZero2 data()[19] 3.220s passed
eqTermCut data()[1] 3.779s passed
divResOne1 data()[20] 3.195s passed
divResOne2 data()[21] 3.231s passed
div_cancel1 data()[22] 3.241s passed
div_cancel2 data()[23] 3.192s passed
divAddMultDenom data()[24] 3.258s passed
divMinus data()[25] 3.246s passed
divMinusDenom data()[26] 3.271s passed
divLeastDPos data()[27] 3.205s passed
divLeastDNeg data()[28] 3.166s passed
divGreatestDPos data()[29] 3.199s passed
equivAllRight data()[2] 3.615s passed
divGreatestDNeg data()[30] 3.167s passed
divIncreasingPos data()[31] 3.196s passed
divIncreasingNeg data()[32] 3.238s passed
jdiv_zero data()[33] 3.199s passed
jdivPulloutMinusNum data()[34] 3.304s passed
jdivPulloutMinusDenom data()[35] 3.200s passed
jdiv_uniquePosPos data()[36] 3.240s passed
jdiv_uniquePosNeg data()[37] 3.230s passed
jdiv_uniqueNegPos data()[38] 3.221s passed
jdiv_uniqueNegNeg data()[39] 3.223s passed
irrflConcrete1 data()[3] 3.421s passed
jdivMultDenom1 data()[40] 3.251s passed
jdivMultDenom2 data()[41] 3.181s passed
mod_geZero data()[42] 3.213s passed
mod_lessDenom data()[43] 3.163s passed
jmod_NumPos data()[44] 3.184s passed
jmod_NumNeg data()[45] 3.209s passed
jmod_geZero data()[46] 3.190s passed
jmodNumZero data()[47] 3.189s passed
jmod_pulloutminusNum data()[48] 3.221s passed
jmod_pulloutminusDenom data()[49] 3.193s passed
irrflConcrete2 data()[4] 3.370s passed
jmodUnique1 data()[50] 3.289s passed
jmodUnique2 data()[51] 3.248s passed
intDivRem data()[52] 3.156s passed
jmodjmod data()[53] 3.212s passed
jmodDivisible data()[54] 3.200s passed
jmodDivisibleRep data()[55] 3.178s passed
jdivAddMultDenom data()[56] 3.314s passed
jmodAltZero data()[57] 3.161s passed
jmodAddMultDenomZero data()[58] 3.284s passed
polyDiv_zero data()[59] 3.218s passed
cancel_gtPos data()[5] 3.396s passed
polyMod_ltdivDenom data()[60] 3.140s passed
bsum_empty data()[61] 3.153s passed
bsum_induction_upper data()[62] 3.167s passed
bsum_induction_lower data()[63] 3.154s passed
bsum_num_of_bounds data()[64] 3.203s passed
bsum_num_of_bounds2 data()[65] 3.209s passed
bsum_induction_upper2 data()[66] 3.186s passed
bsum_induction_upper_concrete data()[67] 3.162s passed
bsum_induction_upper_concrete_2 data()[68] 3.153s passed
bsum_induction_upper2_concrete data()[69] 3.196s passed
cancel_gtNeg data()[6] 3.295s passed
bsum_induction_lower_concrete data()[70] 3.159s passed
bsum_induction_lower2 data()[71] 3.148s passed
bsum_induction_lower2_concrete data()[72] 3.167s passed
bsum_positive data()[73] 3.173s passed
bsum_upper_bound data()[74] 3.224s passed
bsum_lower_bound data()[75] 3.179s passed
bsum_positive_lower_bound_element data()[76] 3.207s passed
bsum_sub_same_index data()[77] 3.193s passed
bsum_less_same_index data()[78] 3.203s passed
bsum_equal_except_one_index data()[79] 3.180s passed
moduloIntIsInInt data()[7] 3.261s passed
bsum_num_of_is_max data()[80] 3.230s passed
bsum_num_of_is_max2 data()[81] 3.189s passed
bsum_num_of_is_max3 data()[82] 3.182s passed
bsum_num_of_is_max4 data()[83] 3.169s passed
bsum_num_of_lt_max data()[84] 3.181s passed
bsum_num_of_lt_max2 data()[85] 3.200s passed
bsum_num_of_lt_max3 data()[86] 3.176s passed
bsum_num_of_lt_max4 data()[87] 3.194s passed
bsum_num_of_gt0 data()[88] 3.225s passed
bsum_num_of_gt0_alt data()[89] 3.184s passed
moduloLongIsInLong data()[8] 3.264s passed
bsum_add_concrete data()[90] 3.182s passed
bprod_all_positive data()[91] 3.169s passed
bprod_split data()[92] 3.148s passed
powConcrete0 data()[93] 3.156s passed
powConcrete1 data()[94] 3.149s passed
powSplitFactor data()[95] 3.142s passed
powAdd data()[96] 3.149s passed
powMono data()[97] 3.134s passed
powMonoConcrete data()[98] 3.166s passed
powMonoConcreteRight data()[99] 3.135s passed
moduloShortIsInShort data()[9] 3.254s passed

Standard output

1956       INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src/test/resources/testcase/dummyTrue.key 
1975       DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 8.94ms 
2191       INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
2204       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)

3102       DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for Meta 
3104       DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for Meta 
3106       DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for Meta 
3106       DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for Meta 
4440       DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for JavaBigintExpression 
9648       DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 7.46s 
9725       INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof dummyTrue.key 
9756       DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 34.3ns 
9768       INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/firstOrder/Taclet_eqTermCut.proof 
9768       DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 203.4ns 
9772       INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
12586      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.81s 
12588      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: eqTermCut 
13515      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: eqTermCut 
13539      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 18.06ms 
13551      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/firstOrder/Taclet_equivAllRight.proof 
13551      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 182.1ns 
13553      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
16278      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.73s 
16278      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: equivAllRight 
17150      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: equivAllRight 
17164      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 10.42ms 
17167      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_irrflConcrete1.proof 
17168      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 161.1ns 
17169      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
19725      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.56s 
19725      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: irrflConcrete1 
20580      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: irrflConcrete1 
20586      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.21ms 
20589      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_irrflConcrete2.proof 
20589      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 314.9ns 
20595      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
23126      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.53s 
23126      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: irrflConcrete2 
23941      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: irrflConcrete2 
23955      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 10.98ms 
23962      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_cancel_gtPos.proof 
23963      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 675ns 
23964      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
26478      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.51s 
26479      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: cancel_gtPos 
27280      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: cancel_gtPos 
27353      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 69.52ms 
27358      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_cancel_gtNeg.proof 
27358      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 167.7ns 
27359      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
29834      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.47s 
29835      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: cancel_gtNeg 
30630      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: cancel_gtNeg 
30650      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 17.12ms 
30653      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intRulesIgnoringOF/Taclet_moduloIntIsInInt.proof 
30654      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 335.6ns 
30655      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
33134      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.48s 
33134      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: moduloIntIsInInt 
33909      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: moduloIntIsInInt 
33913      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 586.6ns 
33915      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intRulesIgnoringOF/Taclet_moduloLongIsInLong.proof 
33915      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 300.7ns 
33916      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
36372      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.46s 
36373      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: moduloLongIsInLong 
37174      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: moduloLongIsInLong 
37177      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 564.9ns 
37179      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intRulesIgnoringOF/Taclet_moduloShortIsInShort.proof 
37179      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 321.3ns 
37180      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
39632      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.45s 
39633      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: moduloShortIsInShort 
40428      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: moduloShortIsInShort 
40431      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 599.5ns 
40433      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intRulesIgnoringOF/Taclet_moduloByteIsInByte.proof 
40434      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 334.3ns 
40435      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
42875      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.44s 
42876      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: moduloByteIsInByte 
43683      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: moduloByteIsInByte 
43689      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.57ms 
43690      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intRulesIgnoringOF/Taclet_moduloCharIsInChar.proof 
43690      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 117.5ns 
43694      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
46116      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.42s 
46117      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: moduloCharIsInChar 
46902      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: moduloCharIsInChar 
46905      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 544.2ns 
46907      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_div_unique1.proof 
46907      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 325.5ns 
46908      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
49434      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.53s 
49434      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: div_unique1 
50254      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: div_unique1 
50293      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 34.95ms 
50294      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_div_unique2.proof 
50295      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 116ns 
50295      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
52732      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.44s 
52732      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: div_unique2 
53512      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: div_unique2 
53545      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 30.25ms 
53547      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_div_exists.proof 
53547      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 193.3ns 
53548      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
55939      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.39s 
55939      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: div_exists 
56727      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: div_exists 
56914      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 177.85ms 
56917      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_div_one.proof 
56917      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 139.4ns 
56918      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
59419      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.5s 
59420      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: div_one 
60190      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: div_one 
60195      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.69ms 
60198      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdiv_one.proof 
60198      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 336.8ns 
60199      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
62614      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.42s 
62615      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdiv_one 
63419      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdiv_one 
63422      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 990.99ns 
63425      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_div_zero.proof 
63426      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 346.6ns 
63426      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
65823      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.4s 
65824      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: div_zero 
66600      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: div_zero 
66636      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 31.86ms 
66640      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divResZero1.proof 
66641      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 326.7ns 
66642      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
69085      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.44s 
69086      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divResZero1 
69867      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divResZero1 
69881      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 11.5ms 
69884      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divResZero2.proof 
69884      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 291.9ns 
69885      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
72294      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.41s 
72294      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divResZero2 
73086      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divResZero2 
73100      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 11.02ms 
73103      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divResOne1.proof 
73103      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 306.8ns 
73104      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
75496      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.39s 
75496      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divResOne1 
76281      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divResOne1 
76296      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 12.62ms 
76297      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divResOne2.proof 
76298      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 116.8ns 
76299      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
78725      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.43s 
78725      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divResOne2 
79512      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divResOne2 
79527      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 11.89ms 
79528      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_div_cancel1.proof 
79529      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 114.6ns 
79529      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
81958      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.43s 
81958      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: div_cancel1 
82744      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: div_cancel1 
82769      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 20.81ms 
82770      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_div_cancel2.proof 
82770      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 114.4ns 
82771      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
85195      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.42s 
85195      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: div_cancel2 
85957      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: div_cancel2 
85960      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.02ms 
85961      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divAddMultDenom.proof 
85961      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 100ns 
85962      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
88395      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.43s 
88395      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divAddMultDenom 
89178      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divAddMultDenom 
89218      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 34.58ms 
89219      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divMinus.proof 
89220      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 112ns 
89220      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
91621      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.4s 
91621      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divMinus 
92403      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divMinus 
92464      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 53.74ms 
92466      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divMinusDenom.proof 
92467      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 234.3ns 
92468      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
94913      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.45s 
94914      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divMinusDenom 
95691      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divMinusDenom 
95735      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 38.37ms 
95736      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divLeastDPos.proof 
95736      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 111.1ns 
95737      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
98148      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.41s 
98148      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divLeastDPos 
98933      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divLeastDPos 
98940      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 5.35ms 
98942      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divLeastDNeg.proof 
98942      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 91.5ns 
98943      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
101340     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.4s 
101340     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divLeastDNeg 
102094     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divLeastDNeg 
102106     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 9.77ms 
102108     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divGreatestDPos.proof 
102108     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 85.3ns 
102108     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
104517     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.41s 
104517     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divGreatestDPos 
105295     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divGreatestDPos 
105305     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 8.05ms 
105306     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divGreatestDNeg.proof 
105307     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 113.2ns 
105307     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
107693     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.39s 
107693     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divGreatestDNeg 
108466     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divGreatestDNeg 
108473     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.8ms 
108474     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divIncreasingPos.proof 
108474     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 81.3ns 
108475     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
110895     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.42s 
110895     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divIncreasingPos 
111661     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divIncreasingPos 
111668     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 5.22ms 
111671     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divIncreasingNeg.proof 
111671     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 298.9ns 
111672     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
114118     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.45s 
114118     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divIncreasingNeg 
114898     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divIncreasingNeg 
114905     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.76ms 
114907     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdiv_zero.proof 
114908     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 95.5ns 
114913     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
117327     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.41s 
117327     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdiv_zero 
118102     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdiv_zero 
118105     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.26ms 
118108     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdivPulloutMinusNum.proof 
118108     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 271.4ns 
118109     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
120627     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.52s 
120628     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdivPulloutMinusNum 
121399     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdivPulloutMinusNum 
121409     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 7.12ms 
121410     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdivPulloutMinusDenom.proof 
121410     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 97.7ns 
121411     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
123775     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.36s 
123775     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdivPulloutMinusDenom 
124551     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdivPulloutMinusDenom 
124606     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 49.58ms 
124613     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdiv_uniquePosPos.proof 
124625     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 12.24ms 
124628     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
127063     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.44s 
127063     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdiv_uniquePosPos 
127833     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdiv_uniquePosPos 
127851     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 14.77ms 
127852     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdiv_uniquePosNeg.proof 
127852     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 79.7ns 
127856     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
130281     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.43s 
130282     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdiv_uniquePosNeg 
131064     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdiv_uniquePosNeg 
131082     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 13.86ms 
131083     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdiv_uniqueNegPos.proof 
131083     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 101.2ns 
131084     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
133509     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.42s 
133509     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdiv_uniqueNegPos 
134285     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdiv_uniqueNegPos 
134302     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 13.62ms 
134303     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdiv_uniqueNegNeg.proof 
134303     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 80.3ns 
134304     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
136721     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.42s 
136721     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdiv_uniqueNegNeg 
137505     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdiv_uniqueNegNeg 
137525     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 15.76ms 
137527     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdivMultDenom1.proof 
137527     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 141.2ns 
137528     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
139957     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.43s 
139958     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdivMultDenom1 
140737     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdivMultDenom1 
140776     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 33.39ms 
140778     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdivMultDenom2.proof 
140779     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 278.1ns 
140780     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
143176     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.4s 
143176     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdivMultDenom2 
143954     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdivMultDenom2 
143957     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 987.49ns 
143958     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_mod_geZero.proof 
143958     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 84.6ns 
143959     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
146386     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.43s 
146386     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: mod_geZero 
147166     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: mod_geZero 
147170     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.4ms 
147172     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_mod_lessDenom.proof 
147172     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 99ns 
147173     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
149551     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.38s 
149552     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: mod_lessDenom 
150326     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: mod_lessDenom 
150333     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 5.33ms 
150334     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmod_NumPos.proof 
150334     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 77.6ns 
150335     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
152733     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.4s 
152733     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmod_NumPos 
153510     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmod_NumPos 
153517     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 5.53ms 
153519     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmod_NumNeg.proof 
153519     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 68.2ns 
153519     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
155927     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.41s 
155927     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmod_NumNeg 
156704     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmod_NumNeg 
156726     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 18.82ms 
156728     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmod_geZero.proof 
156728     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 282.8ns 
156729     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
159130     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.4s 
159130     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmod_geZero 
159909     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmod_geZero 
159917     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 5.47ms 
159918     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmodNumZero.proof 
159918     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 91.6ns 
159919     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
162332     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.41s 
162332     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmodNumZero 
163101     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmodNumZero 
163105     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.26ms 
163108     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmod_pulloutminusNum.proof 
163112     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 3.95ms 
163113     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
165545     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.43s 
165546     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmod_pulloutminusNum 
166322     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmod_pulloutminusNum 
166326     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.65ms 
166328     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmod_pulloutminusDenom.proof 
166328     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 246.1ns 
166329     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
168726     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.4s 
168726     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmod_pulloutminusDenom 
169514     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmod_pulloutminusDenom 
169519     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.98ms 
169521     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmodUnique1.proof 
169521     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 288.8ns 
169522     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
171936     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.41s 
171936     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmodUnique1 
172693     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmodUnique1 
172808     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 106.03ms 
172810     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmodUnique2.proof 
172810     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 251.1ns 
172811     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
175194     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.38s 
175194     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmodUnique2 
175976     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmodUnique2 
176056     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 71.91ms 
176058     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_intDivRem.proof 
176058     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 89.1ns 
176058     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
178430     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.37s 
178430     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: intDivRem 
179209     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: intDivRem 
179212     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.64ms 
179213     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmodjmod.proof 
179214     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 78.6ns 
179214     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
181617     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.4s 
181617     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmodjmod 
182391     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmodjmod 
182424     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 29.71ms 
182426     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmodDivisible.proof 
182426     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 205.8ns 
182426     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
184821     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.39s 
184821     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmodDivisible 
185596     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmodDivisible 
185624     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 25.33ms 
185625     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmodDivisibleRep.proof 
185626     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 74.4ns 
185626     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
188045     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.42s 
188045     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmodDivisibleRep 
188800     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmodDivisibleRep 
188802     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.16ms 
188804     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdivAddMultDenom.proof 
188804     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 61.1ns 
188805     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
191199     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.39s 
191199     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdivAddMultDenom 
191969     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdivAddMultDenom 
192115     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 135.17ms 
192118     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmodAltZero.proof 
192118     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 234ns 
192119     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
194492     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.37s 
194492     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmodAltZero 
195266     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmodAltZero 
195277     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 8.87ms 
195278     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmodAddMultDenomZero.proof 
195278     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 77.2ns 
195279     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
197751     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.47s 
197752     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmodAddMultDenomZero 
198552     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmodAddMultDenomZero 
198562     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 6.07ms 
198563     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_polyDiv_zero.proof 
198563     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 79.2ns 
198564     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
200990     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.43s 
200990     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: polyDiv_zero 
201763     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: polyDiv_zero 
201779     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 13.18ms 
201780     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_polyMod_ltdivDenom.proof 
201780     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 96.6ns 
201781     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
204160     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.38s 
204160     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: polyMod_ltdivDenom 
204908     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: polyMod_ltdivDenom 
204919     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 6ms 
204920     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_empty.proof 
204920     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 70.7ns 
204921     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
207291     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.37s 
207291     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_empty 
208069     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_empty 
208072     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.55ms 
208074     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_induction_upper.proof 
208074     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 79.2ns 
208075     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
210460     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.39s 
210460     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_upper 
211235     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_induction_upper 
211239     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.78ms 
211240     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_induction_lower.proof 
211240     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 73.2ns 
211241     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
213620     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.38s 
213620     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_lower 
214371     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_induction_lower 
214393     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 19.55ms 
214394     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_bounds.proof 
214394     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 84.4ns 
214395     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
216798     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.4s 
216799     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_bounds 
217580     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_bounds 
217596     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 13ms 
217599     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_bounds2.proof 
217599     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 231.7ns 
217601     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
220015     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.41s 
220015     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_bounds2 
220791     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_bounds2 
220806     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 12.11ms 
220808     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_induction_upper2.proof 
220808     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 209.8ns 
220809     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
223214     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.4s 
223214     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_upper2 
223987     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_induction_upper2 
223992     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.42ms 
223994     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_induction_upper_concrete.proof 
223994     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 195.8ns 
223995     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
226379     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.38s 
226380     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_upper_concrete 
227150     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_induction_upper_concrete 
227155     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.56ms 
227156     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_induction_upper_concrete_2.proof 
227157     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 195.6ns 
227157     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
229533     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.38s 
229533     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_upper_concrete_2 
230302     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_induction_upper_concrete_2 
230307     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.42ms 
230308     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_induction_upper2_concrete.proof 
230309     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 69.8ns 
230309     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
232721     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.41s 
232721     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_upper2_concrete 
233500     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_induction_upper2_concrete 
233503     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.33ms 
233504     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_induction_lower_concrete.proof 
233505     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 69.8ns 
233505     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
235887     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.38s 
235887     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_lower_concrete 
236661     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_induction_lower_concrete 
236663     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 636.2ns 
236664     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_induction_lower2.proof 
236664     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 60.6ns 
236665     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
239056     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.39s 
239056     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_lower2 
239807     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_induction_lower2 
239811     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.11ms 
239812     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_induction_lower2_concrete.proof 
239812     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 68.9ns 
239813     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
242208     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.4s 
242208     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_lower2_concrete 
242975     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_induction_lower2_concrete 
242978     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 972.29ns 
242979     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_positive.proof 
242979     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 55.6ns 
242979     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
245335     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.36s 
245335     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_positive 
246104     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_positive 
246150     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 43.65ms 
246152     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_upper_bound.proof 
246152     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 193ns 
246153     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
248562     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.41s 
248562     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_upper_bound 
249310     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_upper_bound 
249374     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 61.63ms 
249376     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_lower_bound.proof 
249379     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 2.92ms 
249380     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
251752     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.37s 
251752     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_lower_bound 
252522     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_lower_bound 
252553     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 28.1ms 
252554     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_positive_lower_bound_element.proof 
252554     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 74.2ns 
252555     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
254925     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.37s 
254926     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_positive_lower_bound_element 
255699     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_positive_lower_bound_element 
255760     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 56.85ms 
255761     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_sub_same_index.proof 
255761     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 68.7ns 
255762     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
258147     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.38s 
258147     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_sub_same_index 
258922     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_sub_same_index 
258953     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 27.57ms 
258954     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_less_same_index.proof 
258954     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 72.3ns 
258955     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
261333     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.38s 
261333     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_less_same_index 
262106     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_less_same_index 
262157     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 46.14ms 
262158     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_equal_except_one_index.proof 
262158     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 73.4ns 
262159     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
264562     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.4s 
264562     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_equal_except_one_index 
265310     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_equal_except_one_index 
265337     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 24.16ms 
265338     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_is_max.proof 
265338     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 84.1ns 
265339     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
267772     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.43s 
267773     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_is_max 
268546     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_is_max 
268567     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 17.46ms 
268568     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_is_max2.proof 
268568     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 77.3ns 
268569     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
270954     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.39s 
270954     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_is_max2 
271729     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_is_max2 
271754     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 22ms 
271757     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_is_max3.proof 
271757     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 185.1ns 
271758     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
274142     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.38s 
274142     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_is_max3 
274918     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_is_max3 
274937     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 16.89ms 
274940     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_is_max4.proof 
274940     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 186.6ns 
274941     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
277308     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.37s 
277308     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_is_max4 
278078     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_is_max4 
278106     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 24.86ms 
278107     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_lt_max.proof 
278107     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 70.8ns 
278108     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
280509     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.4s 
280509     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_lt_max 
281262     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_lt_max 
281287     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 22.12ms 
281288     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_lt_max2.proof 
281289     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 83.2ns 
281289     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
283686     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.4s 
283686     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_lt_max2 
284461     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_lt_max2 
284487     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 23.43ms 
284489     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_lt_max3.proof 
284489     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 79.4ns 
284490     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
286865     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.38s 
286866     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_lt_max3 
287637     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_lt_max3 
287663     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 23.3ms 
287664     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_lt_max4.proof 
287665     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 82.1ns 
287665     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
290072     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.41s 
290072     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_lt_max4 
290834     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_lt_max4 
290858     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 21.2ms 
290859     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_gt0.proof 
290859     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 69.3ns 
290860     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
293281     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.42s 
293281     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_gt0 
294057     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_gt0 
294083     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 22.23ms 
294084     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_gt0_alt.proof 
294084     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 74.7ns 
294085     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
296467     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.38s 
296467     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_gt0_alt 
297241     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_gt0_alt 
297267     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 22.6ms 
297268     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_add_concrete.proof 
297268     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 74.8ns 
297269     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
299664     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.4s 
299665     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_add_concrete 
300441     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_add_concrete 
300448     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 5.72ms 
300449     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bprod/Taclet_bprod_all_positive.proof 
300450     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 62.6ns 
300450     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
302827     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.38s 
302827     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bprod_all_positive 
303599     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bprod_all_positive 
303617     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 15.61ms 
303619     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bprod/Taclet_bprod_split.proof 
303619     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 60.5ns 
303619     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
306007     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.39s 
306007     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bprod_split 
306762     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bprod_split 
306765     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2ms 
306767     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powConcrete0.proof 
306767     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 59.7ns 
306767     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
309150     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.38s 
309151     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powConcrete0 
309918     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powConcrete0 
309921     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 556.95ns 
309922     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powConcrete1.proof 
309923     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 160.49ns 
309923     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
312295     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.37s 
312296     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powConcrete1 
313067     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powConcrete1 
313070     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 704.74ns 
313072     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powSplitFactor.proof 
313072     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 175.28ns 
313073     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
315458     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.39s 
315458     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powSplitFactor 
316205     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powSplitFactor 
316212     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.63ms 
316213     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powAdd.proof 
316213     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 54.6ns 
316214     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
318586     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.37s 
318586     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powAdd 
319355     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powAdd 
319361     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.27ms 
319362     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powMono.proof 
319362     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 62.09ns 
319363     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
321714     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.35s 
321714     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powMono 
322484     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powMono 
322496     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 9.75ms 
322497     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powMonoConcrete.proof 
322497     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 64.7ns 
322498     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
324883     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.39s 
324883     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powMonoConcrete 
325658     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powMonoConcrete 
325661     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.93ms 
325662     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powMonoConcreteRight.proof 
325662     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 54.3ns 
325663     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
328025     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.36s 
328026     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powMonoConcreteRight 
328794     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powMonoConcreteRight 
328796     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 518.89ns 
328798     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powPositive.proof 
328798     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 61ns 
328798     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
331187     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.39s 
331187     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powPositive 
331942     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powPositive 
331947     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.72ms 
331948     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powPositiveConcrete.proof 
331949     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 64.2ns 
331949     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
334341     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.39s 
334341     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powPositiveConcrete 
335118     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powPositiveConcrete 
335120     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 659.48ns 
335122     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powGeq1Concrete.proof 
335122     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 51.2ns 
335122     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
337504     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.38s 
337505     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powGeq1Concrete 
338277     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powGeq1Concrete 
338279     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 577.48ns 
338280     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_pow2InIntLower.proof 
338281     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 58ns 
338281     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
340667     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.39s 
340668     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: pow2InIntLower 
341415     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: pow2InIntLower 
341417     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 587.88ns 
341418     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_pow2InIntUpper.proof 
341418     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 64.3ns 
341419     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
343814     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.4s 
343814     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: pow2InIntUpper 
344586     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: pow2InIntUpper 
344590     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.86ms 
344591     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logSelfConcrete.proof 
344591     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 52.7ns 
344592     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
346960     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.37s 
346960     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logSelfConcrete 
347735     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logSelfConcrete 
347744     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 6.77ms 
347745     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_log1Concrete.proof 
347745     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 66ns 
347746     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
350136     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.39s 
350136     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: log1Concrete 
350905     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: log1Concrete 
350909     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.21ms 
350911     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logProduct.proof 
350911     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 51.8ns 
350911     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
353281     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.37s 
353281     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logProduct 
354050     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logProduct 
354057     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.85ms 
354058     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logTimesBaseConcrete.proof 
354058     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 52.7ns 
354059     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
356434     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.38s 
356435     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logTimesBaseConcrete 
357185     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logTimesBaseConcrete 
357189     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.14ms 
357190     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logProdIdentity.proof 
357191     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 69.8ns 
357191     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
359573     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.38s 
359574     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logProdIdentity 
360349     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logProdIdentity 
360366     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 13.12ms 
360367     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logProdIdentityConcrete.proof 
360367     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 65.1ns 
360368     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
362738     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.37s 
362738     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logProdIdentityConcrete 
363513     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logProdIdentityConcrete 
363516     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.77ms 
363518     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logPowIdentity.proof 
363518     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 60.9ns 
363518     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
365911     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.39s 
365911     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logPowIdentity 
366683     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logPowIdentity 
366686     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.27ms 
366687     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logPowIdentityConcrete.proof 
366687     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 52.3ns 
366687     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
369064     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.38s 
369064     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logPowIdentityConcrete 
369837     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logPowIdentityConcrete 
369840     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.03ms 
369842     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logPositive.proof 
369842     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 60.2ns 
369842     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
372237     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.39s 
372237     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logPositive 
373011     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logPositive 
373028     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 14.42ms 
373029     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logPositiveConcrete.proof 
373029     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 67.4ns 
373030     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
375406     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.38s 
375406     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logPositiveConcrete 
376180     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logPositiveConcrete 
376184     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 539.58ns 
376185     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logMono.proof 
376185     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 63.4ns 
376186     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
378559     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.37s 
378560     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logMono 
379309     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logMono 
379367     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 54.52ms 
379369     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logMonoConcrete.proof 
379369     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 170.19ns 
379370     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
381739     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.37s 
381739     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logMonoConcrete 
382512     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logMonoConcrete 
382515     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.66ms 
382516     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powLogLess.proof 
382517     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 47.5ns 
382517     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
384901     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.38s 
384901     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powLogLess 
385671     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powLogLess 
385693     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 18.82ms 
385695     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powLogMore2.proof 
385695     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 179.9ns 
385696     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
388079     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.38s 
388080     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powLogMore2 
388848     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powLogMore2 
388872     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 21.33ms 
388874     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logLessThanPow.proof 
388874     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 64.8ns 
388874     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
391265     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.39s 
391265     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logLessThanPow 
392033     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logLessThanPow 
392057     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 21.01ms 
392058     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logLessThanPowConcrete.proof 
392058     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 65.9ns 
392059     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
394427     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.37s 
394428     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logLessThanPowConcrete 
395203     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logLessThanPowConcrete 
395205     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 532.78ns 
395206     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logSqueeze.proof 
395206     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 46.5ns 
395207     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
397595     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.39s 
397595     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logSqueeze 
398370     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logSqueeze 
398375     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.9ms 
398377     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/booleanRules/Taclet_ifthenelse_equals.proof 
398377     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 52.9ns 
398377     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
400746     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.37s 
400747     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: ifthenelse_equals 
401518     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: ifthenelse_equals 
401521     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.3ms 
401523     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/booleanRules/Taclet_ifthenelse_equals_1.proof 
401523     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 58.9ns 
401523     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
403925     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.4s 
403925     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: ifthenelse_equals_1 
404696     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: ifthenelse_equals_1 
404698     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 830.28ns 
404700     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/booleanRules/Taclet_ifthenelse_equals_2.proof 
404700     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 47.3ns 
404700     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
407102     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.4s 
407102     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: ifthenelse_equals_2 
407857     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: ifthenelse_equals_2 
407859     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 798.18ns 
407860     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/locSet/Taclet_disjointWithSingleton1.proof 
407860     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 49.3ns 
407861     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
410233     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.37s 
410233     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: disjointWithSingleton1 
411005     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: disjointWithSingleton1 
411008     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.41ms 
411009     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/locSet/Taclet_disjointWithSingleton2.proof 
411009     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 47.1ns 
411010     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
413410     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.4s 
413410     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: disjointWithSingleton2 
414188     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: disjointWithSingleton2 
414191     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.22ms 
414192     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/locSet/Taclet_disjointArrayRanges.proof 
414192     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 106.7ns 
414193     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
416595     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.4s 
416595     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: disjointArrayRanges 
417374     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: disjointArrayRanges 
417384     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 7.45ms 
417385     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/locSet/Taclet_disjointArrayRangeAllFields1.proof 
417385     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 60.7ns 
417386     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
419804     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.42s 
419805     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: disjointArrayRangeAllFields1 
420585     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: disjointArrayRangeAllFields1 
420597     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 10.24ms 
420599     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/locSet/Taclet_disjointArrayRangeAllFields2.proof 
420599     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 56ns 
420600     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
423047     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.45s 
423047     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: disjointArrayRangeAllFields2 
423803     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: disjointArrayRangeAllFields2 
423840     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 34.59ms 
423844     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqSelfDefinition.proof 
423844     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 61.4ns 
423845     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
426214     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.37s 
426215     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqSelfDefinition 
426999     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqSelfDefinition 
427011     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 9.94ms 
427012     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqOutsideValue.proof 
427012     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 67.6ns 
427013     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
429403     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.39s 
429403     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqOutsideValue 
430182     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqOutsideValue 
430186     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.61ms 
430187     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_castedGetAny.proof 
430187     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 57.9ns 
430188     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
432571     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.38s 
432571     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: castedGetAny 
433356     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: castedGetAny 
433362     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.48ms 
433363     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqGetAlphaCast.proof 
433363     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 54.5ns 
433363     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
435733     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.37s 
435733     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqGetAlphaCast 
436516     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqGetAlphaCast 
436518     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 738.18ns 
436519     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqSingleton.proof 
436519     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 55.6ns 
436520     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
438913     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.39s 
438913     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqSingleton 
439690     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqSingleton 
439693     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.24ms 
439694     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqSingletonConcrete.proof 
439694     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 52.9ns 
439695     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
442072     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.38s 
442072     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqSingletonConcrete 
442854     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqSingletonConcrete 
442856     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 773.98ns 
442858     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqConcat.proof 
442858     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 166.8ns 
442859     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
445233     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.37s 
445233     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqConcat 
446016     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqConcat 
446027     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 8.95ms 
446028     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqSub.proof 
446028     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 60.3ns 
446029     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
448453     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.42s 
448454     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqSub 
449233     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqSub 
449237     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.37ms 
449238     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqReverse.proof 
449238     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 56.3ns 
449239     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
451631     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.39s 
451631     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqReverse 
452414     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqReverse 
452421     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.85ms 
452422     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqEmpty.proof 
452422     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 49.9ns 
452422     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
454802     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.38s 
454802     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqEmpty 
455586     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqEmpty 
455588     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 738.48ns 
455589     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqSingleton.proof 
455589     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 52.9ns 
455590     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
457941     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.35s 
457941     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqSingleton 
458716     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqSingleton 
458718     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 596.39ns 
458719     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqConcat.proof 
458719     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 53.8ns 
458719     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
461103     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.38s 
461103     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqConcat 
461886     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqConcat 
461890     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.21ms 
461891     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqSub.proof 
461891     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 56.8ns 
461892     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
464269     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.38s 
464269     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqSub 
465047     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqSub 
465049     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.25ms 
465050     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqReverse.proof 
465050     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 52.2ns 
465051     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
467437     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.39s 
467437     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqReverse 
468218     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqReverse 
468221     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.42ms 
468222     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_equalityToSeqGetAndSeqLenLeft.proof 
468223     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 145.5ns 
468223     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
470615     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.39s 
470616     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: equalityToSeqGetAndSeqLenLeft 
471397     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: equalityToSeqGetAndSeqLenLeft 
471399     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.24ms 
471401     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_equalityToSeqGetAndSeqLenRight.proof 
471401     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 53.7ns 
471401     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
473790     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.39s 
473790     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: equalityToSeqGetAndSeqLenRight 
474552     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: equalityToSeqGetAndSeqLenRight 
474557     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.81ms 
474558     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqSingletonEQ.proof 
474558     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 53.7ns 
474559     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
476937     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.38s 
476937     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqSingletonEQ 
477716     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqSingletonEQ 
477719     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.51ms 
477721     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqConcatEQ.proof 
477721     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 57ns 
477721     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
480113     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.39s 
480114     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqConcatEQ 
480895     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqConcatEQ 
480905     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 8.62ms 
480907     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqSubEQ.proof 
480907     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 60.6ns 
480907     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
483284     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.38s 
483284     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqSubEQ 
484062     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqSubEQ 
484064     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 616.89ns 
484065     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqReverseEQ.proof 
484065     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 52ns 
484066     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
486433     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.37s 
486433     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqReverseEQ 
487213     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqReverseEQ 
487220     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 5.11ms 
487221     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqEmptyEQ.proof 
487221     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 45.6ns 
487222     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
489592     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.37s 
489593     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqEmptyEQ 
490375     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqEmptyEQ 
490377     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 867.28ns 
490378     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqSingletonEQ.proof 
490378     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 76.5ns 
490379     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
492769     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.39s 
492769     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqSingletonEQ 
493555     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqSingletonEQ 
493557     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 825.98ns 
493558     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqConcatEQ.proof 
493558     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 49.5ns 
493559     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
495958     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.4s 
495958     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqConcatEQ 
496743     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqConcatEQ 
496748     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.3ms 
496749     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqSubEQ.proof 
496749     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 59.1ns 
496750     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
499145     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.4s 
499145     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqSubEQ 
499925     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqSubEQ 
499928     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.6ms 
499930     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqReverseEQ.proof 
499930     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 156ns 
499930     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
502305     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.37s 
502305     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqReverseEQ 
503082     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqReverseEQ 
503085     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.78ms 
503087     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqDefEQ.proof 
503087     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 54.7ns 
503087     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
505457     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.37s 
505457     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqDefEQ 
506237     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqDefEQ 
506240     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.18ms 
506242     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqDefEQ.proof 
506242     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 47.5ns 
506242     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
508621     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.38s 
508621     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqDefEQ 
509400     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqDefEQ 
509405     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.1ms 
509406     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqConcatWithSeqEmpty1.proof 
509406     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 52.1ns 
509406     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
511784     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.38s 
511784     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqConcatWithSeqEmpty1 
512563     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqConcatWithSeqEmpty1 
512577     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 12.57ms 
512578     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqConcatWithSeqEmpty2.proof 
512578     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 56.7ns 
512579     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
514972     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.39s 
514973     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqConcatWithSeqEmpty2 
515760     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqConcatWithSeqEmpty2 
515775     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 13.84ms 
515776     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqReverseOfSeqEmpty.proof 
515777     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 65.1ns 
515777     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
518179     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.4s 
518180     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqReverseOfSeqEmpty 
518963     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqReverseOfSeqEmpty 
518973     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 8.66ms 
518974     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_subSeqComplete.proof 
518975     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 51.2ns 
518975     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
521375     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.4s 
521375     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: subSeqComplete 
522158     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: subSeqComplete 
522169     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 9.2ms 
522170     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_subSeqTailR.proof 
522170     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 46.2ns 
522171     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
524563     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.39s 
524563     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: subSeqTailR 
525342     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: subSeqTailR 
525368     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 24.21ms 
525370     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_subSeqTailL.proof 
525370     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 60.8ns 
525370     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
527759     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.39s 
527760     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: subSeqTailL 
528537     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: subSeqTailL 
528562     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 23.63ms 
528563     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_subSeqTailEQR.proof 
528563     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 56.4ns 
528564     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
530944     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.38s 
530944     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: subSeqTailEQR 
531728     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: subSeqTailEQR 
531753     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 22.31ms 
531754     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_subSeqTailEQL.proof 
531754     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 80ns 
531755     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
534148     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.39s 
534148     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: subSeqTailEQL 
534929     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: subSeqTailEQL 
534944     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 12.8ms 
534945     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDef_split.proof 
534945     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 58.4ns 
534945     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
537321     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.38s 
537321     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_split 
538107     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDef_split 
538139     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 28.96ms 
538140     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDef_induction_upper.proof 
538140     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 52.1ns 
538141     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
540538     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.4s 
540538     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_induction_upper 
541325     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDef_induction_upper 
541373     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 44.72ms 
541374     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDef_induction_upper_concrete.proof 
541374     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 59.6ns 
541375     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
543829     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.45s 
543829     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_induction_upper_concrete 
544595     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDef_induction_upper_concrete 
544662     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 63.75ms 
544663     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDef_induction_lower.proof 
544663     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 60.6ns 
544664     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
547050     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.39s 
547050     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_induction_lower 
547825     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDef_induction_lower 
547867     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 39.04ms 
547868     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDef_induction_lower_concrete.proof 
547869     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 58.1ns 
547869     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
550240     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.37s 
550240     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_induction_lower_concrete 
551022     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDef_induction_lower_concrete 
551067     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 41.57ms 
551068     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDef_split_in_three.proof 
551068     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 51.1ns 
551069     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
553439     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.37s 
553439     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_split_in_three 
554215     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDef_split_in_three 
554336     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 112.8ms 
554337     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDef_empty.proof 
554337     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 52ns 
554338     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
556731     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.39s 
556731     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_empty 
557515     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDef_empty 
557522     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 6.09ms 
557524     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDef_one_summand.proof 
557524     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 52.1ns 
557524     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
559929     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.4s 
559929     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_one_summand 
560714     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDef_one_summand 
560722     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 5.95ms 
560723     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDef_lower_equals_upper.proof 
560723     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 71ns 
560724     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
563118     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.39s 
563119     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_lower_equals_upper 
563897     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDef_lower_equals_upper 
563903     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.65ms 
563904     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDefOfSeq.proof 
563904     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 55.2ns 
563904     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
566270     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.37s 
566270     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDefOfSeq 
567047     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDefOfSeq 
567065     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 14.49ms 
567066     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqSelfDefinitionEQ2.proof 
567066     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 49.9ns 
567066     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
569434     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.37s 
569434     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqSelfDefinitionEQ2 
570209     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqSelfDefinitionEQ2 
570219     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 8.77ms 
570220     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_indexOfSeqSingleton.proof 
570220     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 50.1ns 
570221     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
572606     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.38s 
572606     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: indexOfSeqSingleton 
573385     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: indexOfSeqSingleton 
573388     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.68ms 
573389     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_indexOfSeqConcatFirst.proof 
573389     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 55.1ns 
573390     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
575752     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.36s 
575753     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: indexOfSeqConcatFirst 
576528     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: indexOfSeqConcatFirst 
576544     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 14.74ms 
576545     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_indexOfSeqConcatSecond.proof 
576546     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 56.4ns 
576546     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
578937     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.39s 
578937     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: indexOfSeqConcatSecond 
579718     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: indexOfSeqConcatSecond 
579734     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 14.31ms 
579735     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_indexOfSeqSub.proof 
579735     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 52.5ns 
579736     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
582126     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.39s 
582127     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: indexOfSeqSub 
582902     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: indexOfSeqSub 
582920     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 16.35ms 
582922     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfArray2seq.proof 
582922     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 61.2ns 
582922     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
585298     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.38s 
585298     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfArray2seq 
586083     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfArray2seq 
586086     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.25ms 
586087     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getAnyOfArray2seq.proof 
586087     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 58.5ns 
586088     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
588464     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.38s 
588464     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getAnyOfArray2seq 
589246     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getAnyOfArray2seq 
589249     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.13ms 
589250     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfArray2seq.proof 
589250     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 57.6ns 
589251     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
591661     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.41s 
591661     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfArray2seq 
592455     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfArray2seq 
592461     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.68ms 
592462     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_getAnyOfNPermInv.proof 
592462     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 58.9ns 
592463     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
594848     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.39s 
594848     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getAnyOfNPermInv 
595631     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getAnyOfNPermInv 
595637     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.31ms 
595638     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqNPermRange.proof 
595638     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 54.7ns 
595639     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
598069     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.43s 
598070     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqNPermRange 
598854     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqNPermRange 
598925     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 64.78ms 
598926     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermTrans.proof 
598926     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 56.1ns 
598927     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
601349     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.42s 
601349     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermTrans 
602130     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermTrans 
602158     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 25.07ms 
602161     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermRefl.proof 
602161     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 200.3ns 
602161     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
604593     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.43s 
604593     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermRefl 
605370     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermRefl 
605392     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 20.2ms 
605393     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermSplit.proof 
605393     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 60ns 
605394     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
607764     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.37s 
607764     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermSplit 
608543     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermSplit 
608545     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 282.4ns 
608546     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqNPermRight.proof 
608546     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 46.2ns 
608547     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
610912     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.37s 
610912     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqNPermRight 
611712     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqNPermRight 
611913     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 191.86ms 
611915     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermFromSwap.proof 
611915     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 148.4ns 
611916     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
614300     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.38s 
614301     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermFromSwap 
615082     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermFromSwap 
615132     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 45.46ms 
615133     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermTransAlt0.proof 
615133     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 48.6ns 
615134     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
617523     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.39s 
617523     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermTransAlt0 
618305     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermTransAlt0 
618307     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 316.8ns 
618308     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermTransAlt1.proof 
618308     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 47.4ns 
618308     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
620737     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.43s 
620738     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermTransAlt1 
621527     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermTransAlt1 
621529     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 371.59ns 
621531     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermTransAlt2.proof 
621531     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 60.9ns 
621531     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
624009     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.48s 
624009     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermTransAlt2 
624818     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermTransAlt2 
624820     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 332.49ns 
624821     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermTransAlt3.proof 
624821     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 46.4ns 
624822     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
627250     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.43s 
627250     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermTransAlt3 
628033     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermTransAlt3 
628035     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 466.59ns 
628036     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermForall.proof 
628036     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 54.9ns 
628037     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
630434     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.4s 
630434     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermForall 
631217     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermForall 
631293     INFO  Test worker     d.u.i.k.s.SMTFocusResults Analyzing unsat core: (L_1 L_3 L_4) 
631308     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 88.67ms 
631309     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermExists.proof 
631309     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 62.7ns 
631310     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
633717     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.41s 
633717     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermExists 
634502     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermExists 
634549     INFO  Test worker     d.u.i.k.s.SMTFocusResults Analyzing unsat core: (L_1 L_3 L_5 L_6 L_7) 
634550     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 45.95ms 
634551     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm2/Taclet_schiffl_lemma_2.proof 
634551     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 67.3ns 
634552     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
636945     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.39s 
636945     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: schiffl_lemma_2 
637752     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: schiffl_lemma_2 
637755     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.7ns 
637780     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 1: 'macro split-prop' 
637847     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 2: 'rule allRight' 
637866     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 3: 'rule allRight' 
637873     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 4: 'macro split-prop' 
637881     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 5: 'rule 'seqPermDefLeft'' 
637883     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 6: 'rule 'andLeft'' 
637884     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 7: 'rule 'exLeft'' 
637887     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 8: 'macro split-prop' 
637895     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 9: 'rule  seqNPermRange' 
637897     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 10: 'instantiate var=iv with='v_x_0' occ=1' 
637902     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 11: 'rule impLeft' 
637904     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 12: 'tryclose branch' 
638145     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 13: 'rule andLeft' 
638146     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 14: 'rule andLeft' 
638148     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 15: 'instantiate var=iv with='v_y_0' occ=1' 
638149     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 16: 'rule impLeft' 
638150     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 17: 'tryclose branch' 
638267     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 18: 'rule andLeft' 
638268     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 19: 'rule andLeft' 
638268     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 20: 'rule seqNPermDefLeft' 
638270     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 21: 'instantiate var=iv with='v_x_0' occ=2' 
638271     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 22: 'rule impLeft' 
638271     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 23: 'tryclose branch' 
638418     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 24: 'rule exLeft' 
638419     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 25: 'rule andLeft' 
638420     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 26: 'rule andLeft' 
638420     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 27: 'instantiate hide var=iv with='v_y_0' occ=2' 
638421     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 28: 'rule impLeft' 
638422     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 29: 'tryclose branch' 
638572     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 30: 'rule exLeft' 
638573     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 31: 'rule andLeft' 
638574     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 32: 'rule andLeft' 
638574     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 33: 'instantiate var=iv with='jv_0' occ=1' 
638575     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 34: 'rule impLeft' 
638575     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 35: 'tryclose branch' 
638583     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 36: 'rule andLeft' 
638586     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 37: 'rule andLeft' 
638586     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 38: 'rule castAdd formula='s_0[jv_0] = v_x_0' occ=0' 
638588     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 39: 'instantiate hide var=iv with='jv_1' occ=1' 
638590     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 40: 'rule impLeft' 
638591     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 41: 'tryclose branch' 
638599     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 42: 'rule andLeft' 
638600     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 43: 'rule andLeft' 
638601     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 44: 'rule castAdd formula='s_0[jv_1] = v_y_0' occ=0' 
638603     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 45: 'instantiate var=iv  with='v_x_0'' 
638604     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 46: 'rule impLeft' 
638605     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 47: 'tryclose branch' 
638735     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 48: 'instantiate var=iv  with='v_y_0'' 
638735     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 49: 'rule impLeft' 
638737     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 50: 'tryclose branch' 
638834     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 51: 'cut 'v_x_0 = v_y_0'' 
638835     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)'' 
638838     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 53: 'rule andRight' 
638839     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 54: 'rule andRight' 
638840     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 55: 'rule andRight' 
638841     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 56: 'rule andRight' 
638842     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 57: 'rule lenOfSwap' 
638844     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 58: 'tryclose branch' 
638850     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 59: 'rule seqNPermSwapNPerm' 
638851     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 60: 'instantiate hide var='iv' with='v_x_0' occ=1' 
638852     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 61: 'instantiate hide var='jv' with='jv_0'' 
638853     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 62: 'rule impLeft' 
638853     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 63: 'tryclose branch' 
638953     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 64: 'tryclose branch' 
638956     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 65: 'rule allRight' 
638957     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 66: 'rule impRight' 
638958     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 67: 'rule andLeft' 
638959     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 68: 'instantiate var=iv with='v_iv_0'' 
638959     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 69: 'rule impLeft' 
638961     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 70: 'tryclose branch' 
639059     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 71: 'rule getOfSwap' 
639063     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 72: 'rule ifthenelse_negated' 
639064     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 73: 'rule ifthenelse_split occ=0' 
639065     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 74: 'rule andLeft' 
639068     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 75: 'rule andLeft' 
639068     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 76: 'rule andLeft' 
639069     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 77: 'rule ifthenelse_split occ=0' 
639071     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 78: 'tryclose branch' 
639162     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 79: 'rule ifthenelse_split occ=0' 
639163     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 80: 'tryclose branch' 
639241     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 81: 'tryclose branch' 
639244     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 82: 'tryclose branch' 
639248     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 83: 'rule getOfSwap' 
639249     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 84: 'rule ifthenelse_negated' 
639250     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 85: 'rule ifthenelse_split occ=0' 
639251     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 86: 'rule andLeft' 
639252     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 87: 'rule andLeft' 
639252     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 88: 'rule andLeft' 
639253     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 89: 'rule ifthenelse_split occ=0' 
639253     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 90: 'tryclose branch' 
639260     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 91: 'tryclose branch' 
639264     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 92: 'tryclose branch' 
639344     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 93: 'rule getOfSwap' 
639345     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 94: 'rule ifthenelse_negated' 
639347     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 95: 'rule ifthenelse_split occ=0' 
639348     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 96: 'rule andLeft' 
639348     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 97: 'rule andLeft' 
639349     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 98: 'rule andLeft' 
639351     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 99: 'rule ifthenelse_split occ=0' 
639352     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 100: 'tryclose branch' 
639394     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 101: 'tryclose branch' 
639398     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 102: 'tryclose branch' 
639480     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 103: 'cut '(int)s_0[v_x_0] = (int)s_0[v_y_0]'' 
639481     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 104: 'rule seqNPermInjective' 
639483     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 105: 'instantiate hide var=iv with='v_x_0'' 
639484     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 106: 'instantiate hide var=jv with='v_y_0'' 
639485     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 107: 'rule impLeft' 
639485     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 108: 'tryclose branch' 
639604     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 109: 'tryclose branch' 
639607     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 110: 'cut '(int)s_0[v_x_0] = v_x_0'' 
639610     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)'' 
639612     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 112: 'rule andRight' 
639612     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 113: 'rule andRight' 
639613     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 114: 'rule andRight' 
639613     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 115: 'rule andRight' 
639614     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 116: 'tryclose branch' 
639621     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 117: 'rule seqNPermSwapNPerm' 
639626     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 118: 'instantiate hide var=iv with='v_y_0'' 
639628     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 119: 'instantiate hide var=jv with='jv_1'' 
639629     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 120: 'tryclose branch' 
639710     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 121: 'rule allRight' 
639711     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 122: 'rule impRight' 
639712     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 123: 'rule andLeft' 
639713     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 124: 'instantiate var=iv with='v_iv_0'' 
639713     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 125: 'rule impLeft' 
639714     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 126: 'tryclose branch' 
639807     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 127: 'rule getOfSwap' 
639808     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 128: 'rule ifthenelse_negated' 
639809     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 129: 'rule ifthenelse_split occ=0' 
639810     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 130: 'rule andLeft' 
639811     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 131: 'rule andLeft' 
639811     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 132: 'rule andLeft' 
639812     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 133: 'rule ifthenelse_split occ=0' 
639813     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 134: 'tryclose branch' 
639891     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 135: 'rule ifthenelse_split occ=0' 
639892     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 136: 'tryclose branch' 
639959     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 137: 'instantiate var=iv with='v_y_0'' 
639959     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 138: 'rule impLeft' 
639960     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 139: 'tryclose branch' 
639963     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 140: 'tryclose branch' 
639966     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 141: 'tryclose branch' 
639970     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 142: 'tryclose branch' 
640078     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 143: 'rule getOfSwap' 
640080     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 144: 'rule ifthenelse_negated' 
640080     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 145: 'rule ifthenelse_split occ=0' 
640081     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 146: 'tryclose branch' 
640090     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 147: 'tryclose branch' 
640167     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 148: 'tryclose branch' 
643670     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 149: 'cut  '(int)s_0[v_y_0] = v_y_0'' 
643671     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)'' 
643677     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 151: 'rule andRight' 
643678     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 152: 'rule andRight' 
643678     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 153: 'rule andRight' 
643679     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 154: 'rule andRight' 
643679     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 155: 'tryclose branch' 
643687     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 156: 'rule seqNPermSwapNPerm' 
643688     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 157: 'instantiate hide var=iv with='v_x_0'' 
643689     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 158: 'instantiate hide var=jv with='jv_0'' 
643690     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 159: 'rule impLeft' 
643691     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 160: 'tryclose branch' 
643778     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 161: 'tryclose branch' 
643782     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 162: 'rule allRight' 
643783     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 163: 'rule impRight' 
643784     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 164: 'rule andLeft' 
643784     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 165: 'instantiate var=iv with='v_iv_0'' 
643785     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 166: 'rule impLeft' 
643786     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 167: 'tryclose branch' 
643876     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 168: 'rule getOfSwap' 
643878     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 169: 'rule ifthenelse_negated' 
643879     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 170: 'rule ifthenelse_split occ=0' 
643880     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 171: 'rule andLeft' 
643881     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 172: 'rule andLeft' 
643881     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 173: 'rule andLeft' 
643882     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 174: 'rule ifthenelse_split occ=0' 
643883     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 175: 'tryclose branch' 
643996     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 176: 'rule ifthenelse_split occ=0' 
643997     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 177: 'tryclose branch' 
644073     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 178: 'tryclose branch' 
644077     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 179: 'tryclose branch' 
644081     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 180: 'rule getOfSwap' 
644082     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 181: 'rule ifthenelse_negated' 
644083     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 182: 'rule ifthenelse_split occ=0' 
644084     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 183: 'tryclose branch' 
644094     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 184: 'tryclose branch' 
644178     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 185: 'rule getOfSwap' 
644179     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 186: 'rule ifthenelse_negated' 
644180     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 187: 'rule ifthenelse_split occ=0' 
644181     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 188: 'tryclose branch' 
644251     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 189: 'tryclose branch' 
644260     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 190: 'cut '(int)s_0[v_x_0]=v_y_0'' 
644261     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)'' 
644264     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 192: 'rule andRight' 
644265     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 193: 'rule andRight' 
644266     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 194: 'rule andRight' 
644267     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 195: 'rule andRight' 
644267     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 196: 'tryclose branch' 
644278     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 197: 'rule seqNPermSwapNPerm' 
644279     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 198: 'instantiate hide var=iv with='jv_0'' 
644280     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 199: 'instantiate hide var=jv with='v_x_0'' 
644281     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 200: 'rule impLeft' 
644282     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 201: 'tryclose branch' 
644364     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 202: 'rule seqNPermSwapNPerm formula='seqNPerm(seqSwap(s_0, jv_0, v_x_0))'' 
644366     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 203: 'instantiate hide var=iv with='jv_0'' 
644367     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 204: 'instantiate hide var=jv with='v_y_0'' 
644367     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 205: 'rule impLeft' 
644368     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 206: 'tryclose branch' 
644453     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 207: 'tryclose branch' 
644457     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 208: 'rule allRight' 
644458     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 209: 'rule impRight' 
644458     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 210: 'rule andLeft' 
644459     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 211: 'instantiate var=iv with='v_iv_0'' 
644459     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 212: 'rule impLeft' 
644460     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 213: 'tryclose branch' 
644552     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 214: 'rule getOfSwap' 
644554     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 215: 'rule ifthenelse_negated' 
644554     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 216: 'rule ifthenelse_split occ=0' 
644555     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 217: 'rule andLeft' 
644556     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 218: 'rule andLeft' 
644556     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 219: 'rule andLeft' 
644557     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 220: 'rule ifthenelse_split occ=0' 
644557     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 221: 'rule getOfSwap' 
644558     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 222: 'rule ifthenelse_negated' 
644559     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 223: 'rule ifthenelse_split occ=0' 
644560     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 224: 'rule andLeft' 
644560     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 225: 'rule andLeft' 
644560     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 226: 'rule andLeft' 
644561     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 227: 'rule ifthenelse_split occ=0' 
644561     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 228: 'tryclose branch' 
644644     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 229: 'rule ifthenelse_split occ=0' 
644645     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 230: 'tryclose branch' 
644650     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 231: 'tryclose branch' 
644724     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 232: 'tryclose branch' 
644799     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 233: 'rule ifthenelse_split' 
644800     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 234: 'rule getOfSwap' 
644801     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 235: 'rule ifthenelse_negated' 
644801     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 236: 'rule ifthenelse_split occ=0' 
644802     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 237: 'rule andLeft' 
644802     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 238: 'rule andLeft' 
644803     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 239: 'rule andLeft' 
644803     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 240: 'rule ifthenelse_split occ=0' 
644804     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 241: 'tryclose branch' 
644884     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 242: 'tryclose branch' 
644889     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 243: 'tryclose branch' 
644974     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 244: 'rule getOfSwap' 
644975     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 245: 'rule ifthenelse_negated' 
644976     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 246: 'rule ifthenelse_split occ=0' 
644976     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 247: 'rule andLeft' 
644977     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 248: 'rule andLeft' 
644977     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 249: 'rule andLeft' 
644977     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 250: 'rule ifthenelse_split occ=0' 
644978     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 251: 'tryclose branch' 
644983     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 252: 'rule ifthenelse_split occ=0' 
644984     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 253: 'tryclose branch' 
645059     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 254: 'tryclose branch' 
645063     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 255: 'tryclose branch' 
645068     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 256: 'tryclose branch' 
645162     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 257: 'rule getOfSwap' 
645163     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 258: 'rule ifthenelse_negated' 
645163     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 259: 'rule ifthenelse_split occ=0' 
645164     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 260: 'rule andLeft' 
645165     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 261: 'rule andLeft' 
645165     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 262: 'rule andLeft' 
645165     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 263: 'rule ifthenelse_split occ=0' 
645166     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 264: 'tryclose branch' 
645218     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 265: 'rule ifthenelse_split occ=0' 
645219     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 266: 'rule getOfSwap' 
645219     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 267: 'rule ifthenelse_negated' 
645220     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 268: 'rule ifthenelse_split occ=0' 
645220     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 269: 'tryclose branch' 
645225     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 270: 'tryclose branch' 
645230     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 271: 'tryclose branch' 
645405     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 272: 'tryclose branch' 
645523     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 273: 'rule getOfSwap' 
645524     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 274: 'rule ifthenelse_negated' 
645525     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 275: 'rule ifthenelse_split occ=0' 
645526     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 276: 'tryclose branch' 
645751     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 277: 'tryclose branch' 
645847     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 278: 'cut 'int::seqGet(s_0, v_y_0)=v_x_0'' 
645850     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 279: 'tryclose branch' 
649123     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 280: 'rule seqNPermSwapNPerm' 
649128     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 281: 'instantiate hide var=iv with='jv_1'' 
649129     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 282: 'instantiate hide var=jv with='v_y_0'' 
649130     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 283: 'rule impLeft' 
649131     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 284: 'tryclose branch' 
649239     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 285: 'rule seqNPermSwapNPerm formula='seqNPerm(seqSwap(s_0,jv_1,v_y_0))'' 
649241     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 286: 'instantiate hide var=iv with='jv_1'' 
649244     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 287: 'instantiate hide var=jv with='v_x_0'' 
649244     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 288: 'rule impLeft' 
649245     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 289: 'tryclose branch' 
649347     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 290: 'tryclose branch' 
652230     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 291: 'tryclose branch' 
655333     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 292: 'rule seqNPermSwapNPerm formula='seqNPerm(s_0)'' 
655338     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 293: 'instantiate hide var=iv with='v_x_0'' 
655339     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 294: 'instantiate hide var=jv with='jv_0'' 
655339     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 295: 'rule impLeft' 
655340     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 296: 'tryclose branch' 
655447     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 297: 'rule seqNPermSwapNPerm formula='seqNPerm(seqSwap(s_0,v_x_0,jv_0))'' 
655449     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 298: 'instantiate hide var=iv with='v_y_0'' 
655449     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 299: 'instantiate hide var=jv with='jv_1'' 
655450     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)' ...' 
655452     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 301: 'tryclose branch' 
656519     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm2/Taclet_schiffl_thm_1.proof 
656519     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 248.7ns 
656520     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
659012     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.49s 
659012     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: schiffl_thm_1 
659815     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: schiffl_thm_1 
659816     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 7.8ns 
659817     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 1: 'macro split-prop' 
659825     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 2: 'rule schiffl_lemma_2 formula='seqPerm(f_s, f_t)'' 
659836     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 3: 'instantiate hide var=x with='f_x'' 
659839     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 4: 'instantiate hide var=y with='f_y'' 
659841     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 5: 'rule impLeft' 
659841     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 6: 'tryclose branch' 
659845     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 7: 'rule exLeft' 
659847     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 8: 'macro split-prop' 
659850     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 9: 'rule seqPermDef occ=1' 
659853     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 10: 'rule andRight' 
659853     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 11: 'tryclose branch' 
659861     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 12: 'instantiate hide var=s with='r_0'' 
659863     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 13: 'rule andRight' 
659863     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 14: 'tryclose branch' 
659905     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 15: 'rule allRight' 
659906     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 16: 'rule impRight' 
659906     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 17: 'instantiate hide var=iv with='iv_0'' 
659907     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 18: 'rule impLeft' 
659907     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 19: 'tryclose branch' 
659967     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 20: 'rule andLeft' 
659967     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 21: 'rule seqNPermRange' 
659968     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 22: 'instantiate hide var=iv with='iv_0'' 
659969     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 23: 'rule impLeft' 
659970     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 24: 'tryclose branch' 
659973     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 25: 'rule andLeft' 
659973     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 26: 'rule andLeft' 
659973     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 27: 'rule seqNPermRange' 
659974     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 28: 'instantiate hide var=iv with='f_x'' 
659975     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 29: 'rule impLeft' 
659975     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 30: 'tryclose branch' 
660051     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 31: 'rule andLeft' 
660052     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 32: 'rule andLeft' 
660052     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 33: 'rule seqNPermRange' 
660053     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 34: 'instantiate hide var=iv with='f_y'' 
660054     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 35: 'rule impLeft' 
660054     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 36: 'tryclose branch' 
660125     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 37: 'rule andLeft' 
660126     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 38: 'rule andLeft' 
660126     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 39: 'rule getOfSeqDef occ=0' 
660127     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 40: 'rule getOfSeqDef' 
660127     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 41: 'rule ifthenelse_split occ=0' 
660128     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 42: 'rule andLeft occ=0' 
660128     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 43: 'rule sub_zero_2 occ=0' 
660129     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 44: 'rule ifthenelse_split occ=2' 
660129     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 45: 'rule andLeft' 
660130     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 46: 'rule sub_zero_2 occ=0' 
660130     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 47: 'rule add_zero_right occ=0' 
660130     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 48: 'rule add_zero_right occ=0' 
660131     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 49: 'rule add_zero_right occ=0' 
660131     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 50: 'rule add_zero_right occ=0' 
660131     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 51: 'rule add_zero_right occ=0' 
660132     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 52: 'rule add_zero_right occ=0' 
660132     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 53: 'rule ifthenelse_split occ=0' 
660133     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 54: 'rule ifthenelse_split occ=0' 
660133     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 55: 'tryclose branch' 
660135     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 56: 'tryclose branch' 
660165     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 57: 'rule ifthenelse_split occ=0' 
660166     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 58: 'tryclose branch' 
660206     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 59: 'rule ifthenelse_split occ=0' 
660207     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 60: 'rule seqNPermInjective' 
660208     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 61: 'instantiate hide var=iv with='iv_0'' 
660209     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 62: 'instantiate hide var=jv with='f_y'' 
660210     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 63: 'rule impLeft' 
660210     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 64: 'tryclose branch' 
660247     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 65: 'tryclose branch' 
660249     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 66: 'rule ifthenelse_split occ=0' 
660250     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 67: 'rule seqNPermInjective' 
660251     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 68: 'instantiate hide var=iv with='iv_0'' 
660253     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 69: 'instantiate hide var=jv with='f_x'' 
660253     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 70: 'rule impLeft' 
660253     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 71: 'tryclose branch' 
660291     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 72: 'tryclose branch' 
660293     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 73: 'tryclose branch' 
660296     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 74: 'tryclose branch' 
660342     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 75: 'tryclose branch' 
660441     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_eqSameSeq.proof 
660441     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 212.3ns 
660442     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
662877     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.44s 
662877     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: eqSameSeq 
663690     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: eqSameSeq 
663721     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 27.82ms